1  /-
  2  Copyright (c) 2019 Johannes Hölzl. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Johannes Hölzl, Mario Carneiro
  5  -/
  6  import
  7    data.nat.gcd
src    └──────────┘
  8    data.pnat.basic data.int.sqrt data.equiv.encodable
src    └─────────────┘ └───────────┘ └──────────────────┘
  9    algebra.group algebra.ordered_group algebra.group_power
src    └───────────┘ └───────────────────┘ └─────────────────┘
 10    algebra.ordered_field
src    └───────────────────┘
 11    tactic.norm_cast
src    └──────────────┘
 12    tactic.lift
src    └─────────┘
 13  /-!
 14  # Basics for the Rational Numbers
 15  
 16  ## Summary
 17  
 18  We define a rational number `q` as a structure `{ num, denom, pos, cop }`, where
 19  - `num` is the numerator of `q`,
 20  - `denom` is the denominator of `q`,
 21  - `pos` is a proof that `denom > 0`, and
 22  - `cop` is a proof `num` and `denom` are coprime.
 23  
 24  We then define the expected (discrete) field structure on `ℚ` and prove basic lemmas about it.
 25  Moreoever, we provide the expected casts from `ℕ` and `ℤ` into `ℚ`, i.e. `(↑n : ℚ) = n / 1`.
 26  
 27  ## Main Definitions
 28  
 29  - `rat` is the structure encoding `ℚ`.
 30  - `rat.mk n d` constructs a rational number `q = n / d` from `n d : ℤ`.
 31  
 32  ## Notations
 33  
 34  - `/.` is infix notation for `rat.mk`.
 35  
 36  ## Tags
 37  
 38  rat, rationals, field, ℚ, numerator, denominator, num, denom
 39  -/
 40  
 41  /-- `rat`, or `ℚ`, is the type of rational numbers. It is defined
 42    as the set of pairs ⟨n, d⟩ of integers such that `d` is positive and `n` and
 43    `d` are coprime. This representation is preferred to the quotient
 44    because without periodic reduction, the numerator and denominator can grow
 45    exponentially (for example, adding 1/2 to itself repeatedly). -/
 46  structure rat := mk' ::
 47  (num : ℤ)
id          
src         
typ         
 48  (denom : ℕ)
id            
src           
typ           
 49  (pos : 0 < denom)
id             └───┘
src           
typ            └───┘
 50  (cop : num.nat_abs.coprime denom)
id          └─┘└──────┘└──────┘ └───┘
src            └──────┘└──────┘
typ         └─┘└──────┘└──────┘ └───┘
 51  notation `ℚ` := rat
id                   └─┘
src                  └─┘
typ                  └─┘
doc                  └─┘
 52  
 53  namespace rat
 54  
 55  protected def repr : ℚ → string
id                          └────┘
src                         └────┘
typ                         └────┘
doc                       
 56  | ⟨n, d, _, _⟩ := if d = 1 then _root_.repr n else
id                                └─────────┘
src                                 └─────────┘
typ                               └─────────┘
 57    _root_.repr n ++ "/" ++ _root_.repr d
id     └─────────┘   └┘     └┘ └─────────┘
src    └─────────┘   └┘     └┘ └─────────┘
typ    └─────────┘   └┘     └┘ └─────────┘
 58  
 59  instance : has_repr ℚ := ⟨rat.repr⟩
id              └──────┘      └──────┘
src             └──────┘      └──────┘
typ             └──────┘      └──────┘
doc                      
 60  instance : has_to_string ℚ := ⟨rat.repr⟩
id              └───────────┘      └──────┘
src             └───────────┘      └──────┘
typ             └───────────┘      └──────┘
doc                           
 61  meta instance : has_to_format ℚ := ⟨coe ∘ rat.repr⟩
id                   └───────────┘      └─┘  └──────┘
src                  └───────────┘      └─┘  └──────┘
typ                  └───────────┘      └─┘  └──────┘
doc                                
 62  
 63  instance : encodable ℚ := encodable.of_equiv (Σ n : ℤ, {d : ℕ // 0 < d ∧ n.nat_abs.coprime d})
id              └───────┘     └────────────────┘                     └──────┘└──────┘ 
src             └───────┘     └────────────────┘                       └──────┘└──────┘
typ             └───────┘     └────────────────┘                     └──────┘└──────┘ 
doc             └───────┘     └────────────────┘
 64    ⟨λ ⟨a, b, c, d⟩, ⟨a, b, c, d⟩, λ⟨a, b, c, d⟩, ⟨a, b, c, d⟩,
id                                      
typ                                     
 65     λ ⟨a, b, c, d⟩, rfl, λ⟨a, b, c, d⟩, rfl⟩
id                     └─┘                └─┘
src                     └─┘                 └─┘
typ                    └─┘                └─┘
 66  
 67  /-- Embed an integer as a rational number -/
 68  def of_int (n : ℤ) : ℚ :=
id                       
src                      
typ                      
doc                       
 69  ⟨n, 1, nat.one_pos, nat.coprime_one_right _⟩
id         └─────────┘  └───────────────────┘
src         └─────────┘  └───────────────────┘
typ        └─────────┘  └───────────────────┘
 70  
 71  instance : has_zero ℚ := ⟨of_int 0⟩
id              └──────┘      └────┘
src             └──────┘      └────┘
typ             └──────┘      └────┘
doc                           └────┘
 72  instance : has_one ℚ := ⟨of_int 1⟩
id              └─────┘      └────┘
src             └─────┘      └────┘
typ             └─────┘      └────┘
doc                          └────┘
 73  instance : inhabited ℚ := ⟨0⟩
id              └───────┘ 
src             └───────┘ 
typ             └───────┘ 
doc                       
 74  
 75  /-- Form the quotient `n / d` where `n:ℤ` and `d:ℕ+` (not necessarily coprime) -/
 76  def mk_pnat (n : ℤ) : ℕ+ → ℚ | ⟨d, dpos⟩ :=
id                        └┘      
src                       └┘   
typ                       └┘      
doc                        └┘   
 77  let n' := n.nat_abs, g := n'.gcd d in
id       └┘    └──────┘      └┘└──┘
src             └──────┘         └──┘
typ      └┘    └──────┘      └┘└──┘
 78  ⟨n / g, d / g, begin
id           
src           
typ          
st                  └─────
 79    apply (nat.le_div_iff_mul_le _ _ (nat.gcd_pos_of_pos_right _ dpos)).2,
id            └───────────────────┘      └──────────────────────┘   └──┘
src    └────┘ └───────────────────┘└───┘ └──────────────────────┘└─┘    └──┘
typ    └────┘ └───────────────────┘└───┘ └──────────────────────┘└─┘└──┘└──┘
doc    └────┘                      └───┘                         └─┘    └──┘
txt    └────┘                      └───┘                         └─┘    └──┘
par    └────┘                      └───┘                         └─┘    └──┘
pid                               └───┘                         └─┘    └┘└┘
st   ──────────────────────────────────────────────────────────────────────┘└─
 80    simp, exact nat.le_of_dvd dpos (nat.gcd_dvd_right _ _)
id                 └───────────┘ └──┘  └───────────────┘
src    └──┘  └────┘└───────────┘     └───────────────┘└────┘
typ    └──┘  └────┘└───────────┘└──┘ └───────────────┘└────┘
doc    └──┘  └────┘                                   └────┘
txt    └──┘  └────┘                                   └────┘
par    └──┘  └────┘                                   └────┘
pid                                                  └───┘
st   ─────┘└─────────────────────────────────────────────────┘
 81  end, begin
st   └─┘  └─────
 82    have : int.nat_abs (n / ↑g) = n' / g,
id            └─────────┘        └┘   
src    └─────┘└─────────┘   └┘   
typ    └─────┘└─────────┘  └┘└┘ 
doc    └─────┘                └┘    
txt    └─────┘                └┘    
par    └─────┘                └┘    
pid    └───┘└┘                └┘    
st   ─────────────────────────────────────┘└─
 83    { cases int.nat_abs_eq n with e e; rw e, { refl },
id             └────────────┘               
src      └────┘└────────────┘ └───────┘  └─┘     └───┘
typ      └────┘└────────────┘└───────┘  └─┘    └───┘
doc      └────┘               └───────┘  └─┘     └───┘
txt      └────┘               └───────┘  └─┘     └───┘
par      └────┘               └───────┘  └─┘     └───┘
pid                          └───────┘             
st   ───┘└──────────────────────────────────┘└──┘└───┘└┘
 84      rw [int.neg_div_of_dvd, int.nat_abs_neg], { refl },
id           └────────────────┘  └─────────────┘
src      └──┘└────────────────┘└┘└─────────────┘    └───┘
typ      └──┘└────────────────┘└┘└─────────────┘    └───┘
doc      └──┘                  └┘                   └───┘
txt      └──┘                  └┘                   └───┘
par      └──┘                  └┘                   └───┘
pid        └┘                  └┘                       
st   ─────────────────────────┘└───────────────┘└──┘└───┘└┘
 85      exact int.coe_nat_dvd.2 (nat.gcd_dvd_left _ _) },
id             └─────────────┘    └──────────────┘
src      └────┘└─────────────┘└─┘ └──────────────┘└────┘
typ      └────┘└─────────────┘└─┘ └──────────────┘└────┘
doc      └────┘               └─┘                 └────┘
txt      └────┘               └─┘                 └────┘
par      └────┘               └─┘                 └────┘
pid                          └─┘                 └───┘
st   ──────────────────────────────────────────────────┘└┘
 86    rw this,
id        └──┘
src    └─┘
typ    └─┘└──┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────┘└─
 87    exact nat.coprime_div_gcd_div_gcd (nat.gcd_pos_of_pos_right _ dpos)
id           └─────────────────────────┘  └──────────────────────┘   └──┘
src    └────┘└─────────────────────────┘ └──────────────────────┘└─┘    └┘
typ    └────┘└─────────────────────────┘ └──────────────────────┘└─┘└──┘└┘
doc    └────┘                                                    └─┘    └┘
txt    └────┘                                                    └─┘    └┘
par    └────┘                                                    └─┘    └┘
pid                                                             └─┘    
st   ─────────────────────────────────────────────────────────────────────┘
 88  end⟩
st   └─┘
 89  
 90  /-- Form the quotient `n / d` where `n:ℤ` and `d:ℕ`. In the case `d = 0`, we
 91    define `n / 0 = 0` by convention. -/
 92  def mk_nat (n : ℤ) (d : ℕ) : ℚ :=
id                              
src                             
typ                             
doc                               
 93  if d0 : d = 0 then 0 else mk_pnat n ⟨d, nat.pos_of_ne_zero d0⟩
id   └┘                      └─────┘     └────────────────┘ └┘
src  └┘                       └─────┘       └────────────────┘
typ  └┘                      └─────┘     └────────────────┘ └┘
doc                            └─────┘
 94  
 95  /-- Form the quotient `n / d` where `n d : ℤ`. -/
 96  def mk : ℤ → ℤ → ℚ
id                 
src                 
typ                
doc                   
 97  | n (d : ℕ) := mk_nat n d
id               └────┘
src                └────┘
typ              └────┘
doc                 └────┘
 98  | n -[1+ d] := mk_pnat (-n) d.succ_pnat
id      └──┘     └─────┘      └────────┘
src      └──┘      └─────┘      └────────┘
typ     └──┘     └─────┘      └────────┘
doc                 └─────┘       └────────┘
 99  
100  localized "infix ` /. `:70 := rat.mk" in rat
101  
102  theorem mk_pnat_eq (n d h) : mk_pnat n ⟨d, h⟩ = n /. d :=
id                                └─────┘         └┘ 
src                               └─────┘             └┘
typ                               └─────┘         └┘ 
doc                               └─────┘              └┘
103  by change n /. d with dite _ _ _; simp [ne_of_gt h]
id                       └──┘              └──────┘ 
src     └─────┘    └────┘└──┘└────┘  └────┘└──────┘ └─
typ     └─────┘  └────┘└──┘└────┘  └────┘└──────┘└─
doc     └─────┘    └────┘    └────┘  └────┘         └─
txt     └─────┘    └────┘    └────┘  └────┘         └─
par     └─────┘    └────┘    └────┘  └────┘         └─
pid               └────┘    └────┘               
st     └─────────────────────────────────────────────────
104  
src  
typ  
doc  
txt  
par  
pid  
st   
105  theorem mk_nat_eq (n d) : mk_nat n d = n /. d := rfl
id                             └────┘     └┘     └─┘
src                            └────┘        └┘      └─┘
typ                            └────┘     └┘     └─┘
doc                            └────┘         └┘
106  
107  @[simp] theorem mk_zero (n) : n /. 0 = 0 := rfl
id                                  └┘         └─┘
src                                  └┘         └─┘
typ                                 └┘         └─┘
doc    └──┘                          └┘
108  
109  @[simp] theorem zero_mk_pnat (n) : mk_pnat 0 n = 0 :=
id                                      └─────┘    
src                                     └─────┘     
typ                                     └─────┘    
doc    └──┘                             └─────┘
110  by cases n; simp [mk_pnat]; change int.nat_abs 0 with 0; simp *; refl
id                    └─────┘          └─────────┘
src     └────┘   └────┘└─────┘  └─────┘└─────────┘└───────┘  └────┘  └────
typ     └────┘  └────┘└─────┘  └─────┘└─────────┘└───────┘  └────┘  └────
doc     └────┘   └────┘└─────┘  └─────┘           └───────┘  └────┘  └────
txt     └────┘   └────┘         └─────┘           └───────┘  └────┘  └────
par     └────┘   └────┘         └─────┘           └───────┘  └────┘  └────
pid                                           └─────┘            
st     └───────────────────────────────────────────────────────────────────
111  
src  
typ  
doc  
txt  
par  
pid  
st   
112  @[simp] theorem zero_mk_nat (n) : mk_nat 0 n = 0 :=
id                                     └────┘    
src                                    └────┘     
typ                                    └────┘    
doc    └──┘                            └────┘
113  by by_cases n = 0; simp [*, mk_nat]
id                             └────┘
src     └───────┘ └┘  └───────┘└────┘└─
typ     └───────┘└┘  └───────┘└────┘└─
doc     └───────┘  └┘  └───────┘└────┘└─
txt     └───────┘  └┘  └───────┘      └─
par     └───────┘  └┘  └───────┘      └─
pid                     └──┘      
st     └─────────────────────────────────
114  
src  
typ  
doc  
txt  
par  
pid  
st   
115  @[simp] theorem zero_mk (n) : 0 /. n = 0 :=
id                                   └┘  
src                                  └┘   
typ                                  └┘  
doc    └──┘                          └┘
116  by cases n; simp [mk]
id                    └┘
src     └────┘   └────┘└┘└─
typ     └────┘  └────┘└┘└─
doc     └────┘   └────┘└┘└─
txt     └────┘   └────┘  └─
par     └────┘   └────┘  └─
pid                   
st     └───────────────────
117  
src  
typ  
doc  
txt  
par  
pid  
st   
118  private lemma gcd_abs_dvd_left {a b} : (nat.gcd (int.nat_abs a) b : ℤ) ∣ a :=
id                                           └─────┘  └─────────┘         
src                                          └─────┘  └─────────┘          
typ                                          └─────┘  └─────────┘         
119  int.dvd_nat_abs.1 $ int.coe_nat_dvd.2 $ nat.gcd_dvd_left (int.nat_abs a) b
id   └─────────────┘    └─────────────┘    └──────────────┘  └─────────┘   
src  └─────────────┘    └─────────────┘    └──────────────┘  └─────────┘
typ  └─────────────┘    └─────────────┘    └──────────────┘  └─────────┘   
120  
121  @[simp] theorem mk_eq_zero {a b : ℤ} (b0 : b ≠ 0) : a /. b = 0 ↔ a = 0 :=
id                                                     └┘       
src                                                      └┘         
typ                                                    └┘       
doc    └──┘                                                └┘
122  begin
st   └─────
123    constructor; intro h; [skip, {subst a, simp}],
id                                        
src    └─────────┘  └─────┘  └──┘   └────┘   └──┘
typ    └─────────┘  └─────┘  └──┘   └────┘  └──┘
doc    └─────────┘  └─────┘   └──┘   └────┘   └──┘
txt    └─────────┘  └─────┘   └──┘   └────┘   └──┘
par    └─────────┘  └─────┘   └──┘   └────┘   └──┘
pid                      └┘               
st   ──────────────────────────────┘└──────┘└────┘└┘└─
124    have : ∀ {a b}, mk_pnat a b = 0 → a = 0,
id                     └─────┘     
src    └─────┘ └────┘ └─────┘  └─┘   └┘
typ    └─────┘ └────┘ └─────┘  └─┘   └┘
doc    └─────┘ └────┘ └─────┘   └─┘   └┘
txt    └─────┘ └────┘           └─┘   └┘
par    └─────┘ └────┘           └─┘   └┘
pid    └───┘└┘ └────┘           └─┘   
st   ────────────────────────────────────────┘└─
125    { intros a b e, cases b with b h,
id                           
src      └──────────┘  └────┘ └───────┘
typ      └──────────┘  └────┘└───────┘
doc      └──────────┘  └────┘ └───────┘
txt      └──────────┘  └────┘ └───────┘
par      └──────────┘  └────┘ └───────┘
pid            └────┘        └───────┘
st   ───┘└──────────┘└────────────────┘└─
126      injection e with e,
id                 
src      └────────┘ └─────┘
typ      └────────┘└─────┘
doc      └────────┘ └─────┘
txt      └────────┘ └─────┘
par      └────────┘ └─────┘
pid                └─────┘
st   ─────────────────────┘└─
127      apply int.eq_mul_of_div_eq_right gcd_abs_dvd_left e },
id             └────────────────────────┘ └──────────────┘ 
src      └────┘└────────────────────────┘└──────────────┘ 
typ      └────┘└────────────────────────┘└──────────────┘
doc      └────┘                                           
txt      └────┘                                           
par      └────┘                                           
pid                                                      
st   ───────────────────────────────────────────────────────┘└┘
128    cases b with b; simp [mk, mk_nat] at h,
id                          └┘  └────┘
src    └────┘ └─────┘  └────┘└┘└┘└────┘└────┘
typ    └────┘└─────┘  └────┘└┘└┘└────┘└────┘
doc    └────┘ └─────┘  └────┘└┘└┘└────┘└────┘
txt    └────┘ └─────┘  └────┘  └┘      └────┘
par    └────┘ └─────┘  └────┘  └┘      └────┘
pid          └─────┘        └┘      └──┘
st   ───────────────────────────────────────┘└─
129    { simp [mt (congr_arg int.of_nat) b0] at h,
id             └┘  └───────┘ └────────┘  └┘
src      └────┘└┘ └───────┘└────────┘└┘  └────┘
typ      └────┘└┘ └───────┘└────────┘└┘└┘└────┘
doc      └────┘                      └┘  └────┘
txt      └────┘                      └┘  └────┘
par      └────┘                      └┘  └────┘
pid                                └┘  └──┘
st   ───┘└──────────────────────────────────────┘└─
130      exact this h },
id             └──┘ 
src      └────┘     
typ      └────┘└──┘
doc      └────┘     
txt      └────┘     
par      └────┘     
pid                
st   ────────────────┘└┘
131    { apply neg_inj, simp [this h] }
id             └─────┘        └──┘ 
src      └────┘└─────┘  └────┘     └┘
typ      └────┘└─────┘  └────┘└──┘└┘
doc      └────┘         └────┘     └┘
txt      └────┘         └────┘     └┘
par      └────┘         └────┘     └┘
pid                             
st   ────────────────┘└──────────────┘└─
132  end
st   ──┘
133  
134  theorem mk_eq : ∀ {a b c d : ℤ} (hb : b ≠ 0) (hd : d ≠ 0),
id                                                    
src                                                     
typ                                                   
135    a /. b = c /. d ↔ a * d = c * b :=
id      └┘    └┘         
src      └┘      └┘            
typ     └┘    └┘         
doc      └┘       └┘
136  suffices ∀ a b c d hb hd, mk_pnat a ⟨b, hb⟩ = mk_pnat c ⟨d, hd⟩ ↔ a * d = c * b,
id                  └┘ └┘  └─────┘     └┘   └─────┘     └┘         
src                            └─────┘            └─────┘                    
typ                 └┘ └┘  └─────┘     └┘   └─────┘     └┘         
doc                            └─────┘             └─────┘
137  begin
st   └─────
138    intros, cases b with b b; simp [mk, mk_nat, nat.succ_pnat],
id                                    └┘  └────┘  └───────────┘
src    └────┘  └────┘ └───────┘  └────┘└┘└┘└────┘└┘└───────────┘
typ    └────┘  └────┘└───────┘  └────┘└┘└┘└────┘└┘└───────────┘
doc    └────┘  └────┘ └───────┘  └────┘└┘└┘└────┘└┘└───────────┘
txt    └────┘  └────┘ └───────┘  └────┘  └┘      └┘             
par    └────┘  └────┘ └───────┘  └────┘  └┘      └┘             
pid                  └───────┘        └┘      └┘             
st   ───────┘└──────────────────────────────────────────────────┘└─
139    simp [mt (congr_arg int.of_nat) hb],
id           └┘  └───────┘ └────────┘  └┘
src    └────┘└┘ └───────┘└────────┘└┘  
typ    └────┘└┘ └───────┘└────────┘└┘└┘
doc    └────┘                      └┘  
txt    └────┘                      └┘  
par    └────┘                      └┘  
pid                              └┘  
st   ────────────────────────────────────┘└─
140    all_goals {
src    └───────────
typ    └───────────
doc    └───────────
txt    └───────────
par    └───────────
pid             └──
st   ────────────┘
141      cases d with d d; simp [mk, mk_nat, nat.succ_pnat],
id                              └┘  └────┘  └───────────┘
src  ───┘└────┘ └───────┘└┘└────┘└┘└┘└────┘└┘└───────────┘└─
typ  ───┘└────┘└───────┘└┘└────┘└┘└┘└────┘└┘└───────────┘└─
doc  ───┘└────┘ └───────┘└┘└────┘└┘└┘└────┘└┘└───────────┘└─
txt  ───┘└────┘ └───────┘└┘└────┘  └┘      └┘             └─
par  ───┘└────┘ └───────┘└┘└────┘  └┘      └┘             └─
pid  ─────────┘ └───────────────┘  └┘      └┘             └──
st   ─────────────────────────────────────────────────────┘└─
142      simp [mt (congr_arg int.of_nat) hd],
id             └┘  └───────┘ └────────┘  └┘
src  ───┘└────┘└┘ └───────┘└────────┘└┘  └─
typ  ───┘└────┘└┘ └───────┘└────────┘└┘└┘└─
doc  ───┘└────┘                      └┘  └─
txt  ───┘└────┘                      └┘  └─
par  ───┘└────┘                      └┘  └─
pid  ─────────┘                      └┘  └──
st   ──────────────────────────────────────┘└─
143      all_goals { rw this, try {refl} } },
id                      └──┘
src  ───────────────┘└─┘    └┘└───┘└──┘└┘└─┘
typ  ───────────────┘└─┘└──┘└─────┘└──┘└───┘
doc  ───────────────┘└─┘    └┘└───┘└──┘└┘└─┘
txt  ───────────────┘└─┘    └┘└───┘└──┘└┘└─┘
par  ───────────────┘└─┘    └─────┘└──┘└───┘
pid  ──────────────────┘    └──────────────┘
st   ──────────────┘└──────┘└─────────┘ └┘└┘
144    { change a * ↑(d.succ) = -c * ↑b ↔ a * -(d.succ) = c * b,
id                                         └────┘       
src      └─────┘        └┘         └────┘└┘   
typ      └─────┘        └┘        └────┘└┘  
doc      └─────┘          └┘                 └┘   
txt      └─────┘          └┘                 └┘   
par      └─────┘          └┘                 └┘   
pid                      └┘                 └┘   
st   ───┘└────────────────────────────────────────────────────┘└─
145      constructor; intro h; apply neg_inj; simpa [left_distrib, neg_add_eq_iff_eq_add,
id                                   └─────┘         └──────────┘  └───────────────────┘
src      └─────────┘  └─────┘  └────┘└─────┘  └─────┘└──────────┘└┘└───────────────────┘└─
typ      └─────────┘  └─────┘  └────┘└─────┘  └─────┘└──────────┘└┘└───────────────────┘└─
doc      └─────────┘  └─────┘  └────┘         └─────┘            └┘                     └─
txt      └─────────┘  └─────┘  └────┘         └─────┘            └┘                     └─
par      └─────────┘  └─────┘  └────┘         └─────┘            └┘                     └─
pid                        └┘                                 └┘                     └─
st   ─────────────────────────────────────────────────────────────────────────────────────
146        eq_neg_iff_add_eq_zero, neg_eq_iff_add_eq_zero] using h },
id         └────────────────────┘  └────────────────────┘        
src  ─────┘└────────────────────┘└┘└────────────────────┘└──────┘ 
typ  ─────┘└────────────────────┘└┘└────────────────────┘└──────┘
doc  ─────┘                      └┘                      └──────┘ 
txt  ─────┘                      └┘                      └──────┘ 
par  ─────┘                      └┘                      └──────┘ 
pid  ─────┘                      └┘                      └────┘ 
st   ─────────────────────────────────────────────────────────────┘└┘
147    { change -a * ↑d = c * b.succ ↔ a * d = c * -b.succ,
id                                               └────┘
src      └─────┘                      └────┘
typ      └─────┘                   └────┘
doc      └─────┘                     
txt      └─────┘                     
par      └─────┘                     
pid                                 
st   ───┘└───────────────────────────────────────────────┘└─
148      constructor; intro h; apply neg_inj; simpa [left_distrib, eq_comm] using h },
id                                   └─────┘         └──────────┘  └─────┘        
src      └─────────┘  └─────┘  └────┘└─────┘  └─────┘└──────────┘└┘└─────┘└──────┘ 
typ      └─────────┘  └─────┘  └────┘└─────┘  └─────┘└──────────┘└┘└─────┘└──────┘
doc      └─────────┘  └─────┘  └────┘         └─────┘            └┘       └──────┘ 
txt      └─────────┘  └─────┘  └────┘         └─────┘            └┘       └──────┘ 
par      └─────────┘  └─────┘  └────┘         └─────┘            └┘       └──────┘ 
pid                        └┘                                 └┘       └────┘ 
st   ──────────────────────────────────────────────────────────────────────────────┘└┘
149    { change -a * d.succ = -c * b.succ ↔ a * -d.succ = c * -b.succ,
id                                              └────┘       └────┘
src      └─────┘                       └────┘    └────┘
typ      └─────┘                      └────┘   └────┘
doc      └─────┘                                
txt      └─────┘                                
par      └─────┘                                
pid                                            
st   ───────────────────────────────────────────────────────────────┘└─
150      simp [left_distrib] }
id             └──────────┘
src      └────┘└──────────┘└┘
typ      └────┘└──────────┘└┘
doc      └────┘            └┘
txt      └────┘            └┘
par      └────┘            └┘
pid                      
st   ───────────────────────┘└─
151  end,
st   ──┘
152  begin
st   └─────
153    intros, simp [mk_pnat], constructor; intro h,
id                   └─────┘
src    └────┘  └────┘└─────┘  └─────────┘  └─────┘
typ    └────┘  └────┘└─────┘  └─────────┘  └─────┘
doc    └────┘  └────┘└─────┘  └─────────┘  └─────┘
txt    └────┘  └────┘         └─────────┘  └─────┘
par    └────┘  └────┘         └─────────┘  └─────┘
pid                                           └┘
st   ───────┘└──────────────┘└────────────────────┘└─
154    { cases h with ha hb,
id             
src      └────┘ └─────────┘
typ      └────┘└─────────┘
doc      └────┘ └─────────┘
txt      └────┘ └─────────┘
par      └────┘ └─────────┘
pid            └─────────┘
st   ───┘└────────────────┘└─
155      have ha, {
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid      └─────┘
st   ──────────┘└──┘
156        have dv := @gcd_abs_dvd_left,
id                     └──────────────┘
src        └─────────┘ └──────────────┘
typ        └─────────┘ └──────────────┘
doc        └─────────┘
txt        └─────────┘
par        └─────────┘
pid        └─────┘└─┘
st   └────────────────────────────────┘└─
157        have := int.eq_mul_of_div_eq_right dv ha,
id                 └────────────────────────┘ └┘ └┘
src        └──────┘└────────────────────────┘  
typ        └──────┘└────────────────────────┘└┘└┘
doc        └──────┘                            
txt        └──────┘                            
par        └──────┘                            
pid        └───┘└─┘                            
st   ─────────────────────────────────────────────┘└─
158        rw ← int.mul_div_assoc _ dv at this,
id              └───────────────┘   └┘
src        └───┘└───────────────┘└─┘  └──────┘
typ        └───┘└───────────────┘└─┘└┘└──────┘
doc        └───┘                 └─┘  └──────┘
txt        └───┘                 └─┘  └──────┘
par        └───┘                 └─┘  └──────┘
pid          └─┘                 └─┘  └──────┘
st   ────────────────────────────────────────┘└─
159        exact int.eq_mul_of_div_eq_left (dvd_mul_of_dvd_right dv _) this.symm },
id               └───────────────────────┘  └──────────────────┘ └┘    └───────┘
src        └────┘└───────────────────────┘ └──────────────────┘  └──┘└───────┘
typ        └────┘└───────────────────────┘ └──────────────────┘└┘└──┘└───────┘
doc        └────┘                                                └──┘         
txt        └────┘                                                └──┘         
par        └────┘                                                └──┘         
pid                                                             └──┘         
st   ───────────────────────────────────────────────────────────────────────────┘└┘
160      have hb, {
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid      └─────┘
st   ──────────┘└──┘
161        have dv := λ {a b}, nat.gcd_dvd_right (int.nat_abs a) b,
id                             └───────────────┘  └─────────┘
src        └─────────┘ └──────┘└───────────────┘ └─────────┘ └┘
typ        └─────────┘ └──────┘└───────────────┘ └─────────┘ └┘
doc        └─────────┘ └──────┘                              └┘
txt        └─────────┘ └──────┘                              └┘
par        └─────────┘ └──────┘                              └┘
pid        └─────┘└─┘ └──────┘                              └┘
st   └───────────────────────────────────────────────────────────┘└─
162        have := nat.eq_mul_of_div_eq_right dv hb,
id                 └────────────────────────┘ └┘ └┘
src        └──────┘└────────────────────────┘  
typ        └──────┘└────────────────────────┘└┘└┘
doc        └──────┘                            
txt        └──────┘                            
par        └──────┘                            
pid        └───┘└─┘                            
st   ─────────────────────────────────────────────┘└─
163        rw ← nat.mul_div_assoc _ dv at this,
id              └───────────────┘   └┘
src        └───┘└───────────────┘└─┘  └──────┘
typ        └───┘└───────────────┘└─┘└┘└──────┘
doc        └───┘                 └─┘  └──────┘
txt        └───┘                 └─┘  └──────┘
par        └───┘                 └─┘  └──────┘
pid          └─┘                 └─┘  └──────┘
st   ────────────────────────────────────────┘└─
164        exact nat.eq_mul_of_div_eq_left (dvd_mul_of_dvd_right dv _) this.symm },
id               └───────────────────────┘  └──────────────────┘ └┘    └───────┘
src        └────┘└───────────────────────┘ └──────────────────┘  └──┘└───────┘
typ        └────┘└───────────────────────┘ └──────────────────┘└┘└──┘└───────┘
doc        └────┘                                                └──┘         
txt        └────┘                                                └──┘         
par        └────┘                                                └──┘         
pid                                                             └──┘         
st   ───────────────────────────────────────────────────────────────────────────┘└┘
165      have m0 : (a.nat_abs.gcd b * c.nat_abs.gcd d : ℤ) ≠ 0, {
id                  └───────────┘    └───────────┘       
src      └────────┘ └───────────┘  └───────────┘ └─┘ └┘└┘
typ      └────────┘ └───────────┘ └───────────┘└─┘ └┘└┘
doc      └────────┘                              └─┘ └┘ └┘
txt      └────────┘                              └─┘ └┘ └┘
par      └────────┘                              └─┘ └┘ └┘
pid      └─────┘└─┘                              └─┘ └┘ 
st   ────────────────────────────────────────────────────────┘└──┘
166        refine int.coe_nat_ne_zero.2 (ne_of_gt _),
id                └─────────────────┘    └──────┘
src        └─────┘└─────────────────┘└─┘ └──────┘└─┘
typ        └─────┘└─────────────────┘└─┘ └──────┘└─┘
doc        └─────┘                   └─┘         └─┘
txt        └─────┘                   └─┘         └─┘
par        └─────┘                   └─┘         └─┘
pid                                 └─┘         └─┘
st   └─────────────────────────────────────────────┘└─
167        apply mul_pos; apply nat.gcd_pos_of_pos_right; assumption },
id               └─────┘        └──────────────────────┘
src        └────┘└─────┘  └────┘└──────────────────────┘  └─────────┘
typ        └────┘└─────┘  └────┘└──────────────────────┘  └─────────┘
doc        └────┘         └────┘                          └─────────┘
txt        └────┘         └────┘                          └─────────┘
par        └────┘         └────┘                          └─────────┘
pid                                                               
st   ───────────────────────────────────────────────────────────────┘└┘
168      apply eq_of_mul_eq_mul_right m0,
id             └────────────────────┘ └┘
src      └────┘└────────────────────┘
typ      └────┘└────────────────────┘└┘
doc      └────┘                      
txt      └────┘                      
par      └────┘                      
pid                                 
st   ──────────────────────────────────┘└─
169      simpa [mul_comm, mul_left_comm] using
id              └──────┘  └───────────┘
src      └─────┘└──────┘└┘└───────────┘└───────
typ      └─────┘└──────┘└┘└───────────┘└───────
doc      └─────┘        └┘             └───────
txt      └─────┘        └┘             └───────
par      └─────┘        └┘             └───────
pid                   └┘             └─────
st   ──────────────────────────────────────────
170        congr (congr_arg (*) ha.symm) (congr_arg coe hb) },
id         └───┘               └─────┘   └───────┘ └─┘ └┘
src  ─────┘└───┘          └─┘└─────┘└┘ └───────┘└─┘  └┘
typ  ─────┘└───┘          └─┘└─────┘└┘ └───────┘└─┘└┘└┘
doc  ─────┘                └─┘       └┘               └┘
txt  ─────┘                └─┘       └┘               └┘
par  ─────┘                └─┘       └┘               └┘
pid  ─────┘                └─┘       └┘               
st   ──────────────────────────────────────────────────────┘└┘
171    { suffices : ∀ a c, a * d = c * b →
id                               
src      └─────────┘ └──┘         
typ      └─────────┘ └──┘        
doc      └─────────┘ └──┘         
txt      └─────────┘ └──┘         
par      └─────────┘ └──┘         
pid      └───────┘└┘ └──┘         
st   ──────────────────────────────────────
172        a / a.gcd b = c / c.gcd d ∧ b / a.gcd b = d / c.gcd d,
id             └──┘          └──┘                            
src  ─────┘  └──┘     └──┘                  
typ  ─────┘  └──┘     └──┘                 
doc  ─────┘                                  
txt  ─────┘                                  
par  ─────┘                                  
pid  ─────┘                                  
st   ──────────────────────────────────────────────────────────┘└─
173      { cases this a.nat_abs c.nat_abs
id               └──┘ └───────┘ └───────┘
src        └────┘    └───────┘└───────┘
typ        └────┘└──┘└───────┘└───────┘
doc        └────┘                      
txt        └────┘                      
par        └────┘                      
pid                                   
st   ─────┘└──────────────────────────────
174          (by simpa [int.nat_abs_mul] using congr_arg int.nat_abs h) with h₁ h₂,
id                      └─────────────┘        └───────┘ └─────────┘ 
src  ───────┘   └─────┘└─────────────┘└──────┘└───────┘└─────────┘ └──────────┘
typ  ───────┘   └─────┘└─────────────┘└──────┘└───────┘└─────────┘└──────────┘
doc  ───────┘   └─────┘               └──────┘                     └──────────┘
txt  ───────┘   └─────┘               └──────┘                     └──────────┘
par  ───────┘   └─────┘               └──────┘                     └──────────┘
pid  ───────┘   └──────┘               └──────┘                     └─────────┘
st   ──────────┘└────────────────────────────────────────────────────┘└──────────┘└─
175        have hs := congr_arg int.sign h,
id                    └───────┘ └──────┘ 
src        └─────────┘└───────┘└──────┘
typ        └─────────┘└───────┘└──────┘
doc        └─────────┘                 
txt        └─────────┘                 
par        └─────────┘                 
pid        └─────┘└─┘                 
st   ────────────────────────────────────┘└─
176        simp [int.sign_eq_one_of_pos (int.coe_nat_lt.2 hb),
id               └────────────────────┘  └────────────┘   └┘
src        └────┘└────────────────────┘ └────────────┘└─┘  └──
typ        └────┘└────────────────────┘ └────────────┘└─┘└┘└──
doc        └────┘                                     └─┘  └──
txt        └────┘                                     └─┘  └──
par        └────┘                                     └─┘  └──
pid                                                 └─┘  └──
st   ──────────────────────────────────────────────────────────
177              int.sign_eq_one_of_pos (int.coe_nat_lt.2 hd)] at hs,
id               └────────────────────┘  └────────────┘   └┘
src  ───────────┘└────────────────────┘ └────────────┘└─┘  └──────┘
typ  ───────────┘└────────────────────┘ └────────────┘└─┘└┘└──────┘
doc  ───────────┘                                     └─┘  └──────┘
txt  ───────────┘                                     └─┘  └──────┘
par  ───────────┘                                     └─┘  └──────┘
pid  ───────────┘                                     └─┘  └┘└───┘
st   ──────────────────────────────────────────────────────────────┘└─
178        conv in a { rw ← int.sign_mul_nat_abs a },
id                         └──────────────────┘ 
src        └──────┘ └─┘└───┘└──────────────────┘ 
typ        └──────┘└─┘└───┘└──────────────────┘
txt        └──────┘ └─┘└───┘                     
par        └──────┘ └─┘└───┘                     
pid            └─┘ └──────┘                     └┘
st   ────────────────┘└───────────────────────────┘└┘
179        conv in c { rw ← int.sign_mul_nat_abs c },
id                         └──────────────────┘ 
src        └──────┘ └─┘└───┘└──────────────────┘ 
typ        └──────┘└─┘└───┘└──────────────────┘
txt        └──────┘ └─┘└───┘                     
par        └──────┘ └─┘└───┘                     
pid            └─┘ └──────┘                     └┘
st   ────────────────┘└───────────────────────────┘└┘
180        rw [int.mul_div_assoc, int.mul_div_assoc],
id             └───────────────┘  └───────────────┘
src        └──┘└───────────────┘└┘└───────────────┘
typ        └──┘└───────────────┘└┘└───────────────┘
doc        └──┘                 └┘                 
txt        └──┘                 └┘                 
par        └──┘                 └┘                 
pid          └┘                 └┘                 
st   ──────────────────────────┘└─────────────────┘└──
181        exact ⟨congr (congr_arg (*) hs) (congr_arg coe h₁), h₂⟩,
id                └───┘                └┘   └───────┘ └─┘ └┘   └┘
src        └────┘ └───┘           └─┘  └┘ └───────┘└─┘  └─┘  
typ        └────┘ └───┘           └─┘└┘└┘ └───────┘└─┘└┘└─┘└┘
doc        └────┘                 └─┘  └┘               └─┘  
txt        └────┘                 └─┘  └┘               └─┘  
par        └────┘                 └─┘  └┘               └─┘  
pid                              └─┘  └┘               └─┘  
st   ────────────────────────────────────────────────────────────┘└─
182        all_goals { exact int.coe_nat_dvd.2 (nat.gcd_dvd_left _ _) } },
id                           └─────────────┘    └──────────────┘
src        └──────────┘└────┘└─────────────┘└─┘ └──────────────┘└────┘└┘
typ        └──────────┘└────┘└─────────────┘└─┘ └──────────────┘└────┘└┘
doc        └──────────┘└────┘               └─┘                 └────┘└┘
txt        └──────────┘└────┘               └─┘                 └────┘└┘
par        └──────────┘└────┘               └─┘                 └────┘└┘
pid                 └───────┘               └─┘                 └─────┘
st   ────────────────┘└──────────────────────────────────────────────┘└┘
183      intros a c h,
src      └──────────┘
typ      └──────────┘
doc      └──────────┘
txt      └──────────┘
par      └──────────┘
pid            └────┘
st   ───────────────┘└─
184      suffices bd : b / a.gcd b = d / c.gcd d,
id                         └───┘        └───┘ 
src      └────────────┘  └───┘    └───┘
typ      └────────────┘  └───┘   └───┘
doc      └────────────┘                
txt      └────────────┘                
par      └────────────┘                
pid      └─────────┘└─┘                
st   ──────────────────────────────────────────┘└─
185      { refine ⟨_, bd⟩,
id                    └┘
src        └─────┘ └─┘  
typ        └─────┘ └─┘└┘
doc        └─────┘ └─┘  
txt        └─────┘ └─┘  
par        └─────┘ └─┘  
pid               └─┘  
st   ─────┘└────────────┘└─
186        apply nat.eq_of_mul_eq_mul_left hb,
id               └───────────────────────┘ └┘
src        └────┘└───────────────────────┘
typ        └────┘└───────────────────────┘└┘
doc        └────┘                         
txt        └────┘                         
par        └────┘                         
pid                                      
st   ───────────────────────────────────────┘└─
187        rw [← nat.mul_div_assoc _ (nat.gcd_dvd_left _ _), mul_comm,
id               └───────────────┘    └──────────────┘       └──────┘
src        └────┘└───────────────┘└─┘ └──────────────┘└─────┘└──────┘└─
typ        └────┘└───────────────┘└─┘ └──────────────┘└─────┘└──────┘└─
doc        └────┘                 └─┘                 └─────┘        └─
txt        └────┘                 └─┘                 └─────┘        └─
par        └────┘                 └─┘                 └─────┘        └─
pid          └──┘                 └─┘                 └─────┘        └─
st   ─────────────────────────────────────────────────────┘└────────┘└─
188            nat.mul_div_assoc _ (nat.gcd_dvd_right _ _), bd,
id             └───────────────┘    └───────────────┘       └┘
src  ─────────┘└───────────────┘└─┘ └───────────────┘└─────┘  └─
typ  ─────────┘└───────────────┘└─┘ └───────────────┘└─────┘└┘└─
doc  ─────────┘                 └─┘                  └─────┘  └─
txt  ─────────┘                 └─┘                  └─────┘  └─
par  ─────────┘                 └─┘                  └─────┘  └─
pid  ─────────┘                 └─┘                  └─────┘  └─
st   ────────────────────────────────────────────────────┘└──┘└─
189            ← nat.mul_div_assoc _ (nat.gcd_dvd_right _ _), h, mul_comm,
id               └───────────────┘    └───────────────┘         └──────┘
src  ───────────┘└───────────────┘└─┘ └───────────────┘└─────┘ └┘└──────┘└─
typ  ───────────┘└───────────────┘└─┘ └───────────────┘└─────┘└┘└──────┘└─
doc  ───────────┘                 └─┘                  └─────┘ └┘        └─
txt  ───────────┘                 └─┘                  └─────┘ └┘        └─
par  ───────────┘                 └─┘                  └─────┘ └┘        └─
pid  ───────────┘                 └─┘                  └─────┘ └┘        └─
st   ──────────────────────────────────────────────────────┘└─┘└────────┘└─
190            nat.mul_div_assoc _ (nat.gcd_dvd_left _ _)] },
id             └───────────────┘    └──────────────┘
src  ─────────┘└───────────────┘└─┘ └──────────────┘└─────┘
typ  ─────────┘└───────────────┘└─┘ └──────────────┘└─────┘
doc  ─────────┘                 └─┘                 └─────┘
txt  ─────────┘                 └─┘                 └─────┘
par  ─────────┘                 └─┘                 └─────┘
pid  ─────────┘                 └─┘                 └────┘
st   ───────────────────────────────────────────────────┘└┘
191      suffices : ∀ {a c : ℕ} (b>0) (d>0),
src      └─────────┘ └──────┘ └───────────┘ 
typ      └─────────┘ └──────┘ └───────────┘ 
doc      └─────────┘ └──────┘ └───────────┘ 
txt      └─────────┘ └──────┘ └───────────┘ 
par      └─────────┘ └──────┘ └───────────┘ 
pid      └───────┘└┘ └──────┘ └───────────┘ 
st   ────────────────────────────────────────
192        a * d = c * b → b / a.gcd b ≤ d / c.gcd d,
id                             └──┘         └──┘
src  ─────┘           └──┘    └──┘
typ  ─────┘          └──┘    └──┘
doc  ─────┘                        
txt  ─────┘                        
par  ─────┘                        
pid  ─────┘                        
st   ──────────────────────────────────────────────┘└─
193      { exact le_antisymm (this _ hb _ hd h) (this _ hd _ hb h.symm) },
id               └─────────┘                     └──┘   └┘   └┘ └────┘
src        └────┘└─────────┘     └─┘  └─┘   └┘     └─┘  └─┘  └────┘└┘
typ        └────┘└─────────┘     └─┘  └─┘   └┘ └──┘└─┘└┘└─┘└┘└────┘└┘
doc        └────┘                └─┘  └─┘   └┘     └─┘  └─┘        └┘
txt        └────┘                └─┘  └─┘   └┘     └─┘  └─┘        └┘
par        └────┘                └─┘  └─┘   └┘     └─┘  └─┘        └┘
pid                             └─┘  └─┘   └┘     └─┘  └─┘        
st   ─────┘└───────────────────────────────────────────────────────────┘└┘
194      intros a c b hb d hd h,
src      └────────────────────┘
typ      └────────────────────┘
doc      └────────────────────┘
txt      └────────────────────┘
par      └────────────────────┘
pid            └──────────────┘
st   ─────────────────────────┘└─
195      have gb0 := nat.gcd_pos_of_pos_right a hb,
id                   └──────────────────────┘  └┘
src      └──────────┘└──────────────────────┘ 
typ      └──────────┘└──────────────────────┘└┘
doc      └──────────┘                         
txt      └──────────┘                         
par      └──────────┘                         
pid      └──────┘└─┘                         
st   ────────────────────────────────────────────┘└─
196      have gd0 := nat.gcd_pos_of_pos_right c hd,
id                   └──────────────────────┘  └┘
src      └──────────┘└──────────────────────┘ 
typ      └──────────┘└──────────────────────┘└┘
doc      └──────────┘                         
txt      └──────────┘                         
par      └──────────┘                         
pid      └──────┘└─┘                         
st   ────────────────────────────────────────────┘└─
197      apply nat.le_of_dvd,
id             └───────────┘
src      └────┘└───────────┘
typ      └────┘└───────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────────────────┘└─
198      apply (nat.le_div_iff_mul_le _ _ gd0).2,
id              └───────────────────┘     └─┘
src      └────┘ └───────────────────┘└───┘   └─┘
typ      └────┘ └───────────────────┘└───┘└─┘└─┘
doc      └────┘                      └───┘   └─┘
txt      └────┘                      └───┘   └─┘
par      └────┘                      └───┘   └─┘
pid                                 └───┘   └┘
st   ──────────────────────────────────────────┘└─
199      simp, apply nat.le_of_dvd hd (nat.gcd_dvd_right _ _),
id                   └───────────┘ └┘  └───────────────┘
src      └──┘  └────┘└───────────┘   └───────────────┘└───┘
typ      └──┘  └────┘└───────────┘└┘ └───────────────┘└───┘
doc      └──┘  └────┘                                 └───┘
txt      └──┘  └────┘                                 └───┘
par      └──┘  └────┘                                 └───┘
pid                                                  └───┘
st   ───────┘└──────────────────────────────────────────────┘└─
200      apply (nat.coprime_div_gcd_div_gcd gb0).symm.dvd_of_dvd_mul_left,
id              └─────────────────────────┘ └─┘
src      └────┘ └─────────────────────────┘   └────────────────────────┘
typ      └────┘ └─────────────────────────┘└─┘└────────────────────────┘
doc      └────┘                               └────────────────────────┘
txt      └────┘                               └────────────────────────┘
par      └────┘                               └────────────────────────┘
pid                                          └───────────────────────┘
st   ───────────────────────────────────────────────────────────────────┘└─
201      refine ⟨c / c.gcd d, _⟩,
id                   └───┘ 
src      └─────┘   └───┘ └──┘
typ      └─────┘   └───┘└──┘
doc      └─────┘         └──┘
txt      └─────┘         └──┘
par      └─────┘         └──┘
pid                     └──┘
st   ──────────────────────────┘└─
202      rw [← nat.mul_div_assoc _ (nat.gcd_dvd_left _ _),
id             └───────────────┘    └──────────────┘
src      └────┘└───────────────┘└─┘ └──────────────┘└──────
typ      └────┘└───────────────┘└─┘ └──────────────┘└──────
doc      └────┘                 └─┘                 └──────
txt      └────┘                 └─┘                 └──────
par      └────┘                 └─┘                 └──────
pid        └──┘                 └─┘                 └──────
st   ───────────────────────────────────────────────────┘└─
203          ← nat.mul_div_assoc _ (nat.gcd_dvd_right _ _)],
id             └───────────────┘    └───────────────┘
src  ─────────┘└───────────────┘└─┘ └───────────────┘└────┘
typ  ─────────┘└───────────────┘└─┘ └───────────────┘└────┘
doc  ─────────┘                 └─┘                  └────┘
txt  ─────────┘                 └─┘                  └────┘
par  ─────────┘                 └─┘                  └────┘
pid  ─────────┘                 └─┘                  └────┘
st   ────────────────────────────────────────────────────┘└──
204      apply congr_arg (/ c.gcd d),
id             └───────┘   └───┘ 
src      └────┘└───────┘└┘└───┘ 
typ      └────┘└───────┘└┘└───┘
doc      └────┘          └┘      
txt      └────┘          └┘      
par      └────┘          └┘      
pid                     └┘      
st   ──────────────────────────────┘└─
205      rw [mul_comm, ← nat.mul_div_assoc _ (nat.gcd_dvd_left _ _),
id           └──────┘    └───────────────┘    └──────────────┘
src      └──┘└──────┘└──┘└───────────────┘└─┘ └──────────────┘└──────
typ      └──┘└──────┘└──┘└───────────────┘└─┘ └──────────────┘└──────
doc      └──┘        └──┘                 └─┘                 └──────
txt      └──┘        └──┘                 └─┘                 └──────
par      └──┘        └──┘                 └─┘                 └──────
pid        └┘        └──┘                 └─┘                 └──────
st   ───────────────┘└────────────────────────────────────────────┘└─
206          mul_comm, h, nat.mul_div_assoc _ (nat.gcd_dvd_right _ _), mul_comm] }
id           └──────┘    └───────────────┘    └───────────────┘       └──────┘
src  ───────┘└──────┘└┘ └┘└───────────────┘└─┘ └───────────────┘└─────┘└──────┘└┘
typ  ───────┘└──────┘└┘└┘└───────────────┘└─┘ └───────────────┘└─────┘└──────┘└┘
doc  ───────┘        └┘ └┘                 └─┘                  └─────┘        └┘
txt  ───────┘        └┘ └┘                 └─┘                  └─────┘        └┘
par  ───────┘        └┘ └┘                 └─┘                  └─────┘        └┘
pid  ───────┘        └┘ └┘                 └─┘                  └─────┘        
st   ───────────────┘└─┘└───────────────────────────────────────────┘└────────┘└─
207  end
st   ──┘
208  
209  @[simp] theorem div_mk_div_cancel_left {a b c : ℤ} (c0 : c ≠ 0) :
id                                                            
src                                                            
typ                                                           
doc    └──┘
210    (a * c) /. (b * c) = a /. b :=
id          └┘        └┘ 
src           └┘           └┘
typ         └┘        └┘ 
doc            └┘             └┘
211  begin
st   └─────
212    by_cases b0 : b = 0, { subst b0, simp },
id                                └┘
src    └───────┘  └─┘ └┘    └────┘    └───┘
typ    └───────┘  └─┘└┘    └────┘└┘  └───┘
doc    └───────┘  └─┘  └┘    └────┘    └───┘
txt    └───────┘  └─┘  └┘    └────┘    └───┘
par    └───────┘  └─┘  └┘    └────┘    └───┘
pid              └─┘                   
st   ────────────────────┘└──┘└──────┘└─────┘└┘
213    apply (mk_eq (mul_ne_zero b0 c0) b0).2, simp [mul_comm, mul_assoc]
id            └───┘  └─────────┘    └┘  └┘           └──────┘  └───────┘
src    └────┘ └───┘ └─────────┘    └┘  └─┘  └────┘└──────┘└┘└───────┘└┘
typ    └────┘ └───┘ └─────────┘  └┘└┘└┘└─┘  └────┘└──────┘└┘└───────┘└┘
doc    └────┘                      └┘  └─┘  └────┘        └┘         └┘
txt    └────┘                      └┘  └─┘  └────┘        └┘         └┘
par    └────┘                      └┘  └─┘  └────┘        └┘         └┘
pid                               └┘  └┘              └┘         
st   ───────────────────────────────────────┘└───────────────────────────┘
214  end
st   └─┘
215  
216  @[simp] theorem num_denom : ∀ {a : ℚ}, a.num /. a.denom = a
id                                        └──┘ └┘ └────┘  
src                                         └──┘ └┘  └────┘ 
typ                                       └──┘ └┘ └────┘  
doc    └──┘                                      └┘
217  | ⟨n, d, h, (c:_=1)⟩ := show mk_nat n d = _,
id                             └────┘     
src                              └────┘     
typ                            └────┘     
doc                               └────┘
218    by simp [mk_nat, ne_of_gt h, mk_pnat, c]
id              └────┘  └──────┘   └─────┘  
src       └────┘└────┘└┘└──────┘ └┘└─────┘└┘ └─
typ       └────┘└────┘└┘└──────┘└┘└─────┘└┘└─
doc       └────┘└────┘└┘         └┘└─────┘└┘ └─
txt       └────┘      └┘         └┘       └┘ └─
par       └────┘      └┘         └┘       └┘ └─
pid                 └┘         └┘       └┘ 
st       └──────────────────────────────────────
219  
src  
typ  
doc  
txt  
par  
pid  
st   
220  theorem num_denom' {n d h c} : (⟨n, d, h, c⟩ : ℚ) = n /. d := num_denom.symm
id                                                  └┘     └───────┘└───┘
src                                                      └┘      └───────┘└───┘
typ                                                 └┘     └───────┘└───┘
doc                                                       └┘
221  
222  theorem of_int_eq_mk (z : ℤ) : of_int z = z /. 1 := num_denom'
id                                 └────┘    └┘      └────────┘
src                                └────┘      └┘      └────────┘
typ                                └────┘    └┘      └────────┘
doc                                 └────┘       └┘
223  
224  @[elab_as_eliminator] def {u} num_denom_cases_on {C : ℚ → Sort u}
id                                                         
src                                                        
typ                                                        
doc    └────────────────┘                                  
225     : ∀ (a : ℚ) (H : ∀ n d, 0 < d → (int.nat_abs n).coprime d → C (n /. d)), C a
id                                 └─────────┘  └─────┘        └┘      
src                                    └─────────┘   └─────┘           └┘
typ                                └─────────┘  └─────┘        └┘      
doc                                                                     └┘
226  | ⟨n, d, h, c⟩ H := by rw num_denom'; exact H n d h c
id                             └────────┘            
src                         └─┘└────────┘  └────┘     
typ                         └─┘└────────┘  └────┘
doc                         └─┘            └────┘     
txt                         └─┘            └────┘     
par                         └─┘            └────┘     
pid                                                 
st                         └───────────────────────────────
227  
src  
typ  
doc  
txt  
par  
pid  
st   
228  @[elab_as_eliminator] def {u} num_denom_cases_on' {C : ℚ → Sort u}
id                                                          
src                                                         
typ                                                         
doc    └────────────────┘                                   
229     (a : ℚ) (H : ∀ (n:ℤ) (d:ℕ), d ≠ 0 → C (n /. d)) : C a :=
id                                        └┘       
src                                          └┘
typ                                       └┘       
doc                                             └┘
230  num_denom_cases_on a $ λ n d h c,
id   └────────────────┘         
src  └────────────────┘
typ  └────────────────┘         
231  H n d $ ne_of_gt h
id        └──────┘ 
src          └──────┘
typ       └──────┘ 
232  
233  theorem num_dvd (a) {b : ℤ} (b0 : b ≠ 0) : (a /. b).num ∣ a :=
id                                             └┘  └─┘   
src                                              └┘   └─┘  
typ                                            └┘  └─┘   
doc                                                └┘
234  begin
st   └─────
235    cases e : a /. b with n d h c,
id                   
src    └────┘ └─┘    └───────────┘
typ    └────┘ └─┘  └───────────┘
doc    └────┘ └─┘    └───────────┘
txt    └────┘ └─┘    └───────────┘
par    └────┘ └─┘    └───────────┘
pid          └─┘    └───────────┘
st   ──────────────────────────────┘└─
236    rw [rat.num_denom', rat.mk_eq b0
id         └────────────┘  └───────┘ └┘
src    └──┘└────────────┘└┘└───────┘  
typ    └──┘└────────────┘└┘└───────┘└┘
doc    └──┘              └┘           
txt    └──┘              └┘           
par    └──┘              └┘           
pid      └┘              └┘           
st   ───────────────────┘└──────────────
237      (ne_of_gt (int.coe_nat_pos.2 h))] at e,
id        └──────┘  └─────────────┘   
src  ───┘ └──────┘ └─────────────┘└─┘ └──────┘
typ  ───┘ └──────┘ └─────────────┘└─┘└──────┘
doc  ───┘                         └─┘ └──────┘
txt  ───┘                         └─┘ └──────┘
par  ───┘                         └─┘ └──────┘
pid  ───┘                         └─┘ └─┘└───┘
st   ───────────────────────────────────┘└───┘└─
238    refine (int.nat_abs_dvd.1 $ int.dvd_nat_abs.1 $ int.coe_nat_dvd.2 $
id             └─────────────┘     └─────────────┘     └─────────────┘
src    └─────┘ └─────────────┘└─┘ └─────────────┘└─┘ └─────────────┘└─┘ 
typ    └─────┘ └─────────────┘└─┘ └─────────────┘└─┘ └─────────────┘└─┘ 
doc    └─────┘                └─┘                └─┘                └─┘ 
txt    └─────┘                └─┘                └─┘                └─┘ 
par    └─────┘                └─┘                └─┘                └─┘ 
pid                          └─┘                └─┘                └─┘ 
st   ──────────────────────────────────────────────────────────────────────
239      c.dvd_of_dvd_mul_right _),
id       └────────────────────┘
src  ───┘└────────────────────┘└─┘
typ  ───┘└────────────────────┘└─┘
doc  ───┘                      └─┘
txt  ───┘                      └─┘
par  ───┘                      └─┘
pid  ───┘                      └─┘
st   ────────────────────────────┘└─
240    have := congr_arg int.nat_abs e,
id             └───────┘ └─────────┘ 
src    └──────┘└───────┘└─────────┘
typ    └──────┘└───────┘└─────────┘
doc    └──────┘                    
txt    └──────┘                    
par    └──────┘                    
pid    └───┘└─┘                    
st   ────────────────────────────────┘└─
241    simp [int.nat_abs_mul, int.nat_abs_of_nat] at this, simp [this]
id           └─────────────┘  └────────────────┘                 └──┘
src    └────┘└─────────────┘└┘└────────────────┘└───────┘  └────┘    └┘
typ    └────┘└─────────────┘└┘└────────────────┘└───────┘  └────┘└──┘└┘
doc    └────┘               └┘                  └───────┘  └────┘    └┘
txt    └────┘               └┘                  └───────┘  └────┘    └┘
par    └────┘               └┘                  └───────┘  └────┘    └┘
pid                       └┘                  └─────┘          
st   ───────────────────────────────────────────────────┘└────────────┘
242  end
st   └─┘
243  
244  theorem denom_dvd (a b : ℤ) : ((a /. b).denom : ℤ) ∣ b :=
id                                   └┘  └───┘       
src                                   └┘   └───┘      
typ                                  └┘  └───┘       
doc                                    └┘
245  begin
st   └─────
246    by_cases b0 : b = 0, {simp [b0]},
id                               └┘
src    └───────┘  └─┘ └┘   └────┘  
typ    └───────┘  └─┘└┘   └────┘└┘
doc    └───────┘  └─┘  └┘   └────┘  
txt    └───────┘  └─┘  └┘   └────┘  
par    └───────┘  └─┘  └┘   └────┘  
pid              └─┘           
st   ────────────────────┘└──────────┘└┘
247    cases e : a /. b with n d h c,
id                   
src    └────┘ └─┘    └───────────┘
typ    └────┘ └─┘  └───────────┘
doc    └────┘ └─┘    └───────────┘
txt    └────┘ └─┘    └───────────┘
par    └────┘ └─┘    └───────────┘
pid          └─┘    └───────────┘
st   ──────────────────────────────┘└─
248    rw [num_denom', mk_eq b0 (ne_of_gt (int.coe_nat_pos.2 h))] at e,
id         └────────┘  └───┘ └┘  └──────┘  └─────────────┘   
src    └──┘└────────┘└┘└───┘   └──────┘ └─────────────┘└─┘ └──────┘
typ    └──┘└────────┘└┘└───┘└┘ └──────┘ └─────────────┘└─┘└──────┘
doc    └──┘          └┘                                └─┘ └──────┘
txt    └──┘          └┘                                └─┘ └──────┘
par    └──┘          └┘                                └─┘ └──────┘
pid      └┘          └┘                                └─┘ └─┘└───┘
st   ───────────────┘└─────────────────────────────────────────┘└───┘└─
249    refine (int.dvd_nat_abs.1 $ int.coe_nat_dvd.2 $ c.symm.dvd_of_dvd_mul_left _),
id             └─────────────┘     └─────────────┘     └────────────────────────┘
src    └─────┘ └─────────────┘└─┘ └─────────────┘└─┘ └────────────────────────┘└─┘
typ    └─────┘ └─────────────┘└─┘ └─────────────┘└─┘ └────────────────────────┘└─┘
doc    └─────┘                └─┘                └─┘                           └─┘
txt    └─────┘                └─┘                └─┘                           └─┘
par    └─────┘                └─┘                └─┘                           └─┘
pid                          └─┘                └─┘                           └─┘
st   ──────────────────────────────────────────────────────────────────────────────┘└─
250    rw [← int.nat_abs_mul, ← int.coe_nat_dvd, int.dvd_nat_abs, ← e], simp
id           └─────────────┘    └─────────────┘  └─────────────┘    
src    └────┘└─────────────┘└──┘└─────────────┘└┘└─────────────┘└──┘   └───┘
typ    └────┘└─────────────┘└──┘└─────────────┘└┘└─────────────┘└──┘  └───┘
doc    └────┘               └──┘               └┘               └──┘   └───┘
txt    └────┘               └──┘               └┘               └──┘   └───┘
par    └────┘               └──┘               └┘               └──┘   └───┘
pid      └──┘               └──┘               └┘               └──┘       
st   ──────────────────────┘└─────────────────┘└───────────────┘└───┘└──────┘
251  end
st   └─┘
252  
253  protected def add : ℚ → ℚ → ℚ
id                            
src                            
typ                           
doc                            
254  | ⟨n₁, d₁, h₁, c₁⟩ ⟨n₂, d₂, h₂, c₂⟩ := mk_pnat (n₁ * d₂ + n₂ * d₁) ⟨d₁ * d₂, mul_pos h₁ h₂⟩
id      └┘  └┘  └┘       └┘  └┘  └┘         └─────┘                           └─────┘
src                                         └─────┘                           └─────┘
typ     └┘  └┘  └┘       └┘  └┘  └┘         └─────┘                           └─────┘
doc                                         └─────┘
255  
256  instance : has_add ℚ := ⟨rat.add⟩
id              └─────┘      └─────┘
src             └─────┘      └─────┘
typ             └─────┘      └─────┘
doc                     
257  
258  theorem lift_binop_eq (f : ℚ → ℚ → ℚ) (f₁ : ℤ → ℤ → ℤ → ℤ → ℤ) (f₂ : ℤ → ℤ → ℤ → ℤ → ℤ)
id                                                                            
src                                                                           
typ                                                                           
doc                                   
259    (fv : ∀ {n₁ d₁ h₁ c₁ n₂ d₂ h₂ c₂},
id              └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
typ             └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
260      f ⟨n₁, d₁, h₁, c₁⟩ ⟨n₂, d₂, h₂, c₂⟩ = f₁ n₁ d₁ n₂ d₂ /. f₂ n₁ d₁ n₂ d₂)
id         └┘  └┘  └┘  └┘   └┘  └┘  └┘  └┘   └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
src                                                          └┘
typ        └┘  └┘  └┘  └┘   └┘  └┘  └┘  └┘   └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
doc                                                           └┘
261    (f0 : ∀ {n₁ d₁ n₂ d₂} (d₁0 : d₁ ≠ 0) (d₂0 : d₂ ≠ 0), f₂ n₁ d₁ n₂ d₂ ≠ 0)
id              └┘ └┘ └┘ └┘         └┘            └┘      └┘ └┘ └┘ └┘ └┘ 
src                                                                      
typ             └┘ └┘ └┘ └┘         └┘            └┘      └┘ └┘ └┘ └┘ └┘ 
262    (a b c d : ℤ) (b0 : b ≠ 0) (d0 : d ≠ 0)
id                                    
src                                     
typ                                   
263    (H : ∀ {n₁ d₁ n₂ d₂} (h₁ : a * d₁ = n₁ * b) (h₂ : c * d₂ = n₂ * d),
id             └┘ └┘ └┘ └┘          └┘  └┘            └┘  └┘  
src                                                             
typ            └┘ └┘ └┘ └┘          └┘  └┘            └┘  └┘  
264         f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂) :
id          └┘ └┘ └┘ └┘ └┘  └┘      └┘      └┘ └┘ └┘ └┘ └┘
src                                                
typ         └┘ └┘ └┘ └┘ └┘  └┘      └┘      └┘ └┘ └┘ └┘ └┘
265    f (a /. b) (c /. d) = f₁ a b c d /. f₂ a b c d :=
id        └┘     └┘    └┘     └┘ └┘    
src         └┘       └┘                └┘
typ       └┘     └┘    └┘     └┘ └┘    
doc         └┘       └┘                 └┘
266  begin
st   └─────
267    generalize ha : a /. b = x, cases x with n₁ d₁ h₁ c₁, rw num_denom' at ha,
id                                                           └────────┘
src    └──────────────┘        └────┘ └───────────────┘  └─┘└────────┘└────┘
typ    └──────────────┘      └────┘└───────────────┘  └─┘└────────┘└────┘
doc    └──────────────┘        └────┘ └───────────────┘  └─┘          └────┘
txt    └──────────────┘        └────┘ └───────────────┘  └─┘          └────┘
par    └──────────────┘        └────┘ └───────────────┘  └─┘          └────┘
pid              └─┘└┘              └───────────────┘              └────┘
st   ───────────────────────────┘└────────────────────────┘└───────────────────┘└─
268    generalize hc : c /. d = x, cases x with n₂ d₂ h₂ c₂, rw num_denom' at hc,
id                                                           └────────┘
src    └──────────────┘        └────┘ └───────────────┘  └─┘└────────┘└────┘
typ    └──────────────┘      └────┘└───────────────┘  └─┘└────────┘└────┘
doc    └──────────────┘        └────┘ └───────────────┘  └─┘          └────┘
txt    └──────────────┘        └────┘ └───────────────┘  └─┘          └────┘
par    └──────────────┘        └────┘ └───────────────┘  └─┘          └────┘
pid              └─┘└┘              └───────────────┘              └────┘
st   ───────────────────────────┘└────────────────────────┘└───────────────────┘└─
269    rw fv,
src    └─┘
typ    └─┘└┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ──────┘└─
270    have d₁0 := ne_of_gt (int.coe_nat_lt.2 h₁),
id                 └──────┘  └────────────┘   └┘
src    └──────────┘└──────┘ └────────────┘└─┘  
typ    └──────────┘└──────┘ └────────────┘└─┘└┘
doc    └──────────┘                       └─┘  
txt    └──────────┘                       └─┘  
par    └──────────┘                       └─┘  
pid    └──────┘└─┘                       └─┘  
st   ───────────────────────────────────────────┘└─
271    have d₂0 := ne_of_gt (int.coe_nat_lt.2 h₂),
id                 └──────┘  └────────────┘   └┘
src    └──────────┘└──────┘ └────────────┘└─┘  
typ    └──────────┘└──────┘ └────────────┘└─┘└┘
doc    └──────────┘                       └─┘  
txt    └──────────┘                       └─┘  
par    └──────────┘                       └─┘  
pid    └──────┘└─┘                       └─┘  
st   ───────────────────────────────────────────┘└─
272    exact (mk_eq (f0 d₁0 d₂0) (f0 b0 d0)).2 (H ((mk_eq b0 d₁0).1 ha) ((mk_eq d0 d₂0).1 hc))
id                                └┘                     └┘ └─┘    └┘    └───┘ └┘ └─┘    └┘
src    └────┘               └┘       └───┘              └──┘  └┘  └───┘     └──┘  └─┘
typ    └────┘               └┘ └┘    └───┘        └┘└─┘└──┘└┘└┘  └───┘└┘└─┘└──┘└┘└─┘
doc    └────┘               └┘       └───┘              └──┘  └┘            └──┘  └─┘
txt    └────┘               └┘       └───┘              └──┘  └┘            └──┘  └─┘
par    └────┘               └┘       └───┘              └──┘  └┘            └──┘  └─┘
pid                        └┘       └───┘              └──┘  └┘            └──┘  └┘
st   ─────────────────────────────────────────────────────────────────────────────────────────┘
273  end
st   └─┘
274  
275  @[simp] theorem add_def {a b c d : ℤ} (b0 : b ≠ 0) (d0 : d ≠ 0) :
id                                                          
src                                                           
typ                                                         
doc    └──┘
276    a /. b + c /. d = (a * d + c * b) /. (b * d) :=
id      └┘    └┘            └┘    
src      └┘      └┘                 └┘    
typ     └┘    └┘            └┘    
doc      └┘       └┘                     └┘
277  begin
st   └─────
278    apply lift_binop_eq rat.add; intros; try {assumption},
id           └───────────┘ └─────┘
src    └────┘└───────────┘└─────┘  └────┘  └───┘└────────┘
typ    └────┘└───────────┘└─────┘  └────┘  └───┘└────────┘
doc    └────┘                      └────┘  └───┘└────────┘
txt    └────┘                      └────┘  └───┘└────────┘
par    └────┘                      └────┘  └───┘└────────┘
pid                                          └───────────┘
st   ───────────────────────────────────────────┘└────────┘└┘
279    { apply mk_pnat_eq },
id             └────────┘
src      └────┘└────────┘
typ      └────┘└────────┘
doc      └────┘          
txt      └────┘          
par      └────┘          
pid                     
st   ───┘└───────────────┘└┘
280    { apply mul_ne_zero d₁0 d₂0 },
id             └─────────┘ └─┘ └─┘
src      └────┘└─────────┘      
typ      └────┘└─────────┘└─┘└─┘
doc      └────┘                 
txt      └────┘                 
par      └────┘                 
pid                            
st   ───┘└────────────────────────┘└┘
281    calc (n₁ * d₂ + n₂ * d₁) * (b * d) =
id     └──┘                    
src    └──┘                    
typ    └──┘                    
doc    └──┘
st   ───────────────────────────────────────
282            (n₁ * b) * d₂ * d + (n₂ * d) * (d₁ * b) : by simp [mul_add, mul_comm, mul_left_comm]
id              └┘        └┘        └┘        └┘                └─────┘  └──────┘  └───────────┘
src                                                         └────┘└─────┘└┘└──────┘└┘└───────────┘└─
typ             └┘        └┘        └┘        └┘          └────┘└─────┘└┘└──────┘└┘└───────────┘└─
doc                                                         └────┘       └┘        └┘             └─
txt                                                         └────┘       └┘        └┘             └─
par                                                         └────┘       └┘        └┘             └─
pid                                                                    └┘        └┘             
st   ─────────────────────────────────────────────────────┘└────────────────────────────────────────
283      ... = (a * d₁) * d₂ * d + (c * d₂) * (d₁ * b) : by rw [h₁, h₂]
id                                                              └┘  └┘
src  ───┘                                                   └──┘  └┘  └─
typ  ───┘                                                   └──┘└┘└┘└┘└─
doc  ───┘                                                   └──┘  └┘  └─
txt  ───┘                                                   └──┘  └┘  └─
par  ───┘                                                   └──┘  └┘  └─
pid  ───┘                                                     └┘  └┘  
st   ───┘└────────────────────────────────────────────────┘└─────┘└──┘
284      ... = (a * d + c * b) * (d₁ * d₂)             : by simp [mul_add, mul_comm, mul_left_comm]
id                                                              └─────┘  └──────┘  └───────────┘
src  ───┘                                                   └────┘└─────┘└┘└──────┘└┘└───────────┘└┘
typ  ───┘                                                 └────┘└─────┘└┘└──────┘└┘└───────────┘└┘
doc  ───┘                                                   └────┘       └┘        └┘             └┘
txt  ───┘                                                   └────┘       └┘        └┘             └┘
par  ───┘                                                   └────┘       └┘        └┘             └┘
pid  ───┘                                                              └┘        └┘             
st   ───┘└────────────────────────────────────────────────┘└───────────────────────────────────────┘
285  end
st   └─┘
286  
287  protected def neg : ℚ → ℚ
id                         
src                         
typ                        
doc                         
288  | ⟨n, d, h, c⟩ := ⟨-n, d, h, by simp [c]⟩
id                                     
src                                 └────┘ 
typ                              └────┘
doc                                  └────┘ 
txt                                  └────┘ 
par                                  └────┘ 
pid                                       
st                                  └───────┘
289  
290  instance : has_neg ℚ := ⟨rat.neg⟩
id              └─────┘      └─────┘
src             └─────┘      └─────┘
typ             └─────┘      └─────┘
doc                     
291  
292  @[simp] theorem neg_def {a b : ℤ} : -(a /. b) = -a /. b :=
id                                        └┘     └┘ 
src                                        └┘       └┘
typ                                       └┘     └┘ 
doc    └──┘                                  └┘         └┘
293  begin
st   └─────
294    by_cases b0 :  b = 0, { subst b0, simp, refl },
id                                 └┘
src    └───────┘  └──┘ └┘    └────┘    └──┘  └───┘
typ    └───────┘  └──┘└┘    └────┘└┘  └──┘  └───┘
doc    └───────┘  └──┘  └┘    └────┘    └──┘  └───┘
txt    └───────┘  └──┘  └┘    └────┘    └──┘  └───┘
par    └───────┘  └──┘  └┘    └────┘    └──┘  └───┘
pid              └──┘                         
st   ─────────────────────┘└──┘└──────┘└────┘└─────┘└┘
295    generalize ha : a /. b = x, cases x with n₁ d₁ h₁ c₁, rw num_denom' at ha,
id                                                           └────────┘
src    └──────────────┘        └────┘ └───────────────┘  └─┘└────────┘└────┘
typ    └──────────────┘      └────┘└───────────────┘  └─┘└────────┘└────┘
doc    └──────────────┘        └────┘ └───────────────┘  └─┘          └────┘
txt    └──────────────┘        └────┘ └───────────────┘  └─┘          └────┘
par    └──────────────┘        └────┘ └───────────────┘  └─┘          └────┘
pid              └─┘└┘              └───────────────┘              └────┘
st   ───────────────────────────┘└────────────────────────┘└───────────────────┘└─
296    show rat.mk' _ _ _ _ = _, rw num_denom',
id          └─────┘                 └────────┘
src    └───┘└─────┘└───────┘ └┘  └─┘└────────┘
typ    └───┘└─────┘└───────┘ └┘  └─┘└────────┘
doc    └───┘       └───────┘ └┘  └─┘
txt    └───┘       └───────┘ └┘  └─┘
par    └───┘       └───────┘ └┘  └─┘
pid    └───┘       └───────┘ └┘    
st   ─────────────────────────┘└─────────────┘└─
297    have d0 := ne_of_gt (int.coe_nat_lt.2 h₁),
id                └──────┘  └────────────┘   └┘
src    └─────────┘└──────┘ └────────────┘└─┘  
typ    └─────────┘└──────┘ └────────────┘└─┘└┘
doc    └─────────┘                       └─┘  
txt    └─────────┘                       └─┘  
par    └─────────┘                       └─┘  
pid    └─────┘└─┘                       └─┘  
st   ──────────────────────────────────────────┘└─
298    apply (mk_eq d0 b0).2, have h₁ := (mk_eq b0 d0).1 ha,
id            └───┘ └┘ └┘                 └───┘ └┘ └┘    └┘
src    └────┘ └───┘    └─┘  └─────────┘ └───┘    └──┘
typ    └────┘ └───┘└┘└┘└─┘  └─────────┘ └───┘└┘└┘└──┘└┘
doc    └────┘          └─┘  └─────────┘          └──┘
txt    └────┘          └─┘  └─────────┘          └──┘
par    └────┘          └─┘  └─────────┘          └──┘
pid                   └┘  └─────┘└─┘          └──┘
st   ──────────────────────┘└─────────────────────────────┘└─
299    simp only [neg_mul_eq_neg_mul_symm, congr_arg has_neg.neg h₁]
id                └─────────────────────┘  └───────┘ └─────────┘ └┘
src    └─────────┘└─────────────────────┘└┘└───────┘└─────────┘  └┘
typ    └─────────┘└─────────────────────┘└┘└───────┘└─────────┘└┘└┘
doc    └─────────┘                       └┘                      └┘
txt    └─────────┘                       └┘                      └┘
par    └─────────┘                       └┘                      └┘
pid        └──┘└┘                       └┘                      
st   ───────────────────────────────────────────────────────────────┘
300  end
st   └─┘
301  
302  protected def mul : ℚ → ℚ → ℚ
id                            
src                            
typ                           
doc                            
303  | ⟨n₁, d₁, h₁, c₁⟩ ⟨n₂, d₂, h₂, c₂⟩ := mk_pnat (n₁ * n₂) ⟨d₁ * d₂, mul_pos h₁ h₂⟩
id      └┘  └┘  └┘       └┘  └┘  └┘         └─────┘                   └─────┘
src                                         └─────┘                   └─────┘
typ     └┘  └┘  └┘       └┘  └┘  └┘         └─────┘                   └─────┘
doc                                         └─────┘
304  
305  instance : has_mul ℚ := ⟨rat.mul⟩
id              └─────┘      └─────┘
src             └─────┘      └─────┘
typ             └─────┘      └─────┘
doc                     
306  
307  @[simp] theorem mul_def {a b c d : ℤ} (b0 : b ≠ 0) (d0 : d ≠ 0) :
id                                                          
src                                                           
typ                                                         
doc    └──┘
308    (a /. b) * (c /. d) = (a * c) /. (b * d) :=
id       └┘      └┘         └┘    
src       └┘        └┘            └┘    
typ      └┘      └┘         └┘    
doc       └┘         └┘              └┘
309  begin
st   └─────
310    apply lift_binop_eq rat.mul; intros; try {assumption},
id           └───────────┘ └─────┘
src    └────┘└───────────┘└─────┘  └────┘  └───┘└────────┘
typ    └────┘└───────────┘└─────┘  └────┘  └───┘└────────┘
doc    └────┘                      └────┘  └───┘└────────┘
txt    └────┘                      └────┘  └───┘└────────┘
par    └────┘                      └────┘  └───┘└────────┘
pid                                          └───────────┘
st   ───────────────────────────────────────────┘└────────┘└┘
311    { apply mk_pnat_eq },
id             └────────┘
src      └────┘└────────┘
typ      └────┘└────────┘
doc      └────┘          
txt      └────┘          
par      └────┘          
pid                     
st   ───┘└───────────────┘└┘
312    { apply mul_ne_zero d₁0 d₂0 },
id             └─────────┘ └─┘ └─┘
src      └────┘└─────────┘      
typ      └────┘└─────────┘└─┘└─┘
doc      └────┘                 
txt      └────┘                 
par      └────┘                 
pid                            
st   ───┘└────────────────────────┘└┘
313    cc
src    └─┘
typ    └─┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────┘
314  end
st   └─┘
315  
316  protected def inv : ℚ → ℚ
id                         
src                         
typ                        
doc                         
317  | ⟨(n+1:ℕ), d, h, c⟩ := ⟨d, n+1, n.succ_pos, c.symm⟩
id                               └───────┘   └───┘
src                                 └───────┘   └───┘
typ                              └───────┘   └───┘
318  | ⟨0, d, h, c⟩ := 0
319  | ⟨-[1+ n], d, h, c⟩ := ⟨-d, n+1, n.succ_pos, nat.coprime.symm $ by simp; exact c⟩
id      └──┘                       └───────┘  └──────────────┘                  
src     └──┘                         └───────┘  └──────────────┘      └──┘  └────┘
typ     └──┘                       └───────┘  └──────────────┘      └──┘  └────┘
doc                                                                      └──┘  └────┘
txt                                                                      └──┘  └────┘
par                                                                      └──┘  └────┘
pid                                                                                 
st                                                                      └────────────┘
320  
321  instance : has_inv ℚ := ⟨rat.inv⟩
id              └─────┘      └─────┘
src             └─────┘      └─────┘
typ             └─────┘      └─────┘
doc                     
322  
323  @[simp] theorem inv_def {a b : ℤ} : (a /. b)⁻¹ = b /. a :=
id                                        └┘  └┘   └┘ 
src                                        └┘   └┘    └┘
typ                                       └┘  └┘   └┘ 
doc    └──┘                                 └┘          └┘
324  begin
st   └─────
325    by_cases a0 : a = 0, { subst a0, simp, refl },
id                                └┘
src    └───────┘  └─┘ └┘    └────┘    └──┘  └───┘
typ    └───────┘  └─┘└┘    └────┘└┘  └──┘  └───┘
doc    └───────┘  └─┘  └┘    └────┘    └──┘  └───┘
txt    └───────┘  └─┘  └┘    └────┘    └──┘  └───┘
par    └───────┘  └─┘  └┘    └────┘    └──┘  └───┘
pid              └─┘                         
st   ────────────────────┘└──┘└──────┘└────┘└─────┘└┘
326    by_cases b0 : b = 0, { subst b0, simp, refl },
id                                 └┘
src    └───────┘  └─┘  └┘    └────┘    └──┘  └───┘
typ    └───────┘  └─┘ └┘    └────┘└┘  └──┘  └───┘
doc    └───────┘  └─┘  └┘    └────┘    └──┘  └───┘
txt    └───────┘  └─┘  └┘    └────┘    └──┘  └───┘
par    └───────┘  └─┘  └┘    └────┘    └──┘  └───┘
pid              └─┘                         
st   ────────────────────┘└──┘└──────┘└────┘└─────┘└┘
327    generalize ha : a /. b = x, cases x with n d h c, rw num_denom' at ha,
id                                                       └────────┘
src    └──────────────┘        └────┘ └───────────┘  └─┘└────────┘└────┘
typ    └──────────────┘      └────┘└───────────┘  └─┘└────────┘└────┘
doc    └──────────────┘        └────┘ └───────────┘  └─┘          └────┘
txt    └──────────────┘        └────┘ └───────────┘  └─┘          └────┘
par    └──────────────┘        └────┘ └───────────┘  └─┘          └────┘
pid              └─┘└┘              └───────────┘              └────┘
st   ───────────────────────────┘└────────────────────┘└───────────────────┘└─
328    refine eq.trans (_ : rat.inv ⟨n, d, h, c⟩ = d /. n) _,
id            └──────┘      └─────┘                  
src    └─────┘└──────┘ └──┘└─────┘  └┘ └┘ └┘ └┘     └─┘
typ    └─────┘└──────┘ └──┘└─────┘  └┘ └┘└┘└┘   └─┘
doc    └─────┘         └──┘         └┘ └┘ └┘ └┘     └─┘
txt    └─────┘         └──┘         └┘ └┘ └┘ └┘     └─┘
par    └─────┘         └──┘         └┘ └┘ └┘ └┘     └─┘
pid                   └──┘         └┘ └┘ └┘ └┘     └─┘
st   ──────────────────────────────────────────────────────┘└─
329    { cases n with n; [cases n with n, skip],
id                            
src      └────┘ └─────┘  └────┘ └─────┘  └──┘
typ      └────┘└─────┘  └────┘└─────┘  └──┘
doc      └────┘ └─────┘   └────┘ └─────┘  └──┘
txt      └────┘ └─────┘   └────┘ └─────┘  └──┘
par      └────┘ └─────┘   └────┘ └─────┘  └──┘
pid            └─────┘         └─────┘
st   ───┘└────────────────────────────────────┘└─
330      { refl },
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid            
st   ─────┘└───┘└┘
331      { change int.of_nat n.succ with (n+1:ℕ),
id                └────────┘ └────┘       
src        └─────┘└────────┘└────┘└────┘  └┘ 
typ        └─────┘└────────┘└────┘└────┘ └┘ 
doc        └─────┘                └────┘   └┘ 
txt        └─────┘                └────┘   └┘ 
par        └─────┘                └────┘   └┘ 
pid                              └────┘   └┘ 
st   ─────┘└───────────────────────────────────┘└─
332        unfold rat.inv, rw num_denom' },
id                            └────────┘
src        └────────────┘  └─┘└────────┘
typ        └────────────┘  └─┘└────────┘
doc        └────────────┘  └─┘          
txt        └────────────┘  └─┘          
par        └────────────┘  └─┘          
pid              └──────┘              
st   ───────────────────┘└──────────────┘└┘
333      { unfold rat.inv, rw num_denom', refl } },
id                            └────────┘
src        └────────────┘  └─┘└────────┘  └───┘
typ        └────────────┘  └─┘└────────┘  └───┘
doc        └────────────┘  └─┘            └───┘
txt        └────────────┘  └─┘            └───┘
par        └────────────┘  └─┘            └───┘
pid              └──────┘                    
st   ───────────────────┘└─────────────┘└─────┘└──┘
334    have n0 : n ≠ 0,
id                
src    └────────┘ └┘
typ    └────────┘└┘
doc    └────────┘  └┘
txt    └────────┘  └┘
par    └────────┘  └┘
pid    └─────┘└─┘  
st   ────────────────┘└─
335    { refine mt (λ (n0 : n = 0), _) a0,
id              └┘                   └┘
src      └─────┘└┘  └─────┘  └──────┘
typ      └─────┘└┘  └─────┘└──────┘└┘
doc      └─────┘    └─────┘  └──────┘
txt      └─────┘    └─────┘  └──────┘
par      └─────┘    └─────┘  └──────┘
pid                └─────┘  └──────┘
st   ───┘└──────────────────────────────┘└─
336      subst n0, simp at ha,
id             └┘
src      └────┘    └────────┘
typ      └────┘└┘  └────────┘
doc      └────┘    └────────┘
txt      └────┘    └────────┘
par      └────┘    └────────┘
pid                   └───┘
st   ───────────┘└──────────┘└─
337      exact (mk_eq_zero b0).1 ha },
id              └────────┘ └┘    └┘
src      └────┘ └────────┘  └──┘  
typ      └────┘ └────────┘└┘└──┘└┘
doc      └────┘             └──┘  
txt      └────┘             └──┘  
par      └────┘             └──┘  
pid                        └──┘  
st   ──────────────────────────────┘└┘
338    have d0 := ne_of_gt (int.coe_nat_lt.2 h),
id                └──────┘  └────────────┘   
src    └─────────┘└──────┘ └────────────┘└─┘ 
typ    └─────────┘└──────┘ └────────────┘└─┘
doc    └─────────┘                       └─┘ 
txt    └─────────┘                       └─┘ 
par    └─────────┘                       └─┘ 
pid    └─────┘└─┘                       └─┘ 
st   ─────────────────────────────────────────┘└─
339    have ha := (mk_eq b0 d0).1 ha,
id                 └───┘ └┘ └┘    └┘
src    └─────────┘ └───┘    └──┘
typ    └─────────┘ └───┘└┘└┘└──┘└┘
doc    └─────────┘          └──┘
txt    └─────────┘          └──┘
par    └─────────┘          └──┘
pid    └─────┘└─┘          └──┘
st   ──────────────────────────────┘└─
340    apply (mk_eq n0 a0).2,
id            └───┘ └┘ └┘
src    └────┘ └───┘    └─┘
typ    └────┘ └───┘└┘└┘└─┘
doc    └────┘          └─┘
txt    └────┘          └─┘
par    └────┘          └─┘
pid                   └┘
st   ──────────────────────┘└─
341    cc
src    └─┘
typ    └─┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────┘
342  end
st   └─┘
343  
344  variables (a b c : ℚ)
id                      
src                     
typ                     
doc                     
345  
346  protected theorem add_zero : a + 0 = a :=
id                                     
src                                    
typ                                    
347  num_denom_cases_on' a $ λ n d h,
id   └─────────────────┘        
src  └─────────────────┘
typ  └─────────────────┘        
348  by rw [← zero_mk d]; simp [h, -zero_mk]
id            └─────┘          
src     └────┘└─────┘   └────┘ └───────────
typ     └────┘└─────┘  └────┘└───────────
doc     └────┘          └────┘ └───────────
txt     └────┘          └────┘ └───────────
par     └────┘          └────┘ └───────────
pid       └──┘               └─────────┘
st     └──────────────┘└────────────────────
349  
src  
typ  
doc  
txt  
par  
pid  
st   
350  protected theorem zero_add : 0 + a = a :=
id                                     
src                                    
typ                                    
351  num_denom_cases_on' a $ λ n d h,
id   └─────────────────┘        
src  └─────────────────┘
typ  └─────────────────┘        
352  by rw [← zero_mk d]; simp [h, -zero_mk]
id            └─────┘          
src     └────┘└─────┘   └────┘ └───────────
typ     └────┘└─────┘  └────┘└───────────
doc     └────┘          └────┘ └───────────
txt     └────┘          └────┘ └───────────
par     └────┘          └────┘ └───────────
pid       └──┘               └─────────┘
st     └──────────────┘└────────────────────
353  
src  
typ  
doc  
txt  
par  
pid  
st   
354  protected theorem add_comm : a + b = b + a :=
id                                      
src                                       
typ                                     
355  num_denom_cases_on' a $ λ n₁ d₁ h₁,
id   └─────────────────┘      └┘ └┘ └┘
src  └─────────────────┘
typ  └─────────────────┘      └┘ └┘ └┘
356  num_denom_cases_on' b $ λ n₂ d₂ h₂,
id   └─────────────────┘      └┘ └┘ └┘
src  └─────────────────┘
typ  └─────────────────┘      └┘ └┘ └┘
357  by simp [h₁, h₂, mul_comm]
id            └┘  └┘  └──────┘
src     └────┘  └┘  └┘└──────┘└─
typ     └────┘└┘└┘└┘└┘└──────┘└─
doc     └────┘  └┘  └┘        └─
txt     └────┘  └┘  └┘        └─
par     └────┘  └┘  └┘        └─
pid           └┘  └┘        
st     └────────────────────────
358  
src  
typ  
doc  
txt  
par  
pid  
st   
359  protected theorem add_assoc : a + b + c = a + (b + c) :=
id                                            
src                                               
typ                                           
360  num_denom_cases_on' a $ λ n₁ d₁ h₁,
id   └─────────────────┘      └┘ └┘ └┘
src  └─────────────────┘
typ  └─────────────────┘      └┘ └┘ └┘
361  num_denom_cases_on' b $ λ n₂ d₂ h₂,
id   └─────────────────┘      └┘ └┘ └┘
src  └─────────────────┘
typ  └─────────────────┘      └┘ └┘ └┘
362  num_denom_cases_on' c $ λ n₃ d₃ h₃,
id   └─────────────────┘      └┘ └┘ └┘
src  └─────────────────┘
typ  └─────────────────┘      └┘ └┘ └┘
363  by simp [h₁, h₂, h₃, mul_ne_zero, mul_add, mul_comm, mul_left_comm, add_left_comm]
id            └┘  └┘  └┘  └─────────┘  └─────┘  └──────┘  └───────────┘  └───────────┘
src     └────┘  └┘  └┘  └┘└─────────┘└┘└─────┘└┘└──────┘└┘└───────────┘└┘└───────────┘└─
typ     └────┘└┘└┘└┘└┘└┘└┘└─────────┘└┘└─────┘└┘└──────┘└┘└───────────┘└┘└───────────┘└─
doc     └────┘  └┘  └┘  └┘           └┘       └┘        └┘             └┘             └─
txt     └────┘  └┘  └┘  └┘           └┘       └┘        └┘             └┘             └─
par     └────┘  └┘  └┘  └┘           └┘       └┘        └┘             └┘             └─
pid           └┘  └┘  └┘           └┘       └┘        └┘             └┘             
st     └────────────────────────────────────────────────────────────────────────────────
364  
src  
typ  
doc  
txt  
par  
pid  
st   
365  protected theorem add_left_neg : -a + a = 0 :=
id                                       
src                                        
typ                                      
366  num_denom_cases_on' a $ λ n d h,
id   └─────────────────┘        
src  └─────────────────┘
typ  └─────────────────┘        
367  by simp [h]
id            
src     └────┘ └─
typ     └────┘└─
doc     └────┘ └─
txt     └────┘ └─
par     └────┘ └─
pid          
st     └─────────
368  
src  
typ  
doc  
txt  
par  
pid  
st   
369  protected theorem mul_one : a * 1 = a :=
id                                    
src                                   
typ                                   
370  num_denom_cases_on' a $ λ n d h,
id   └─────────────────┘        
src  └─────────────────┘
typ  └─────────────────┘        
371  by change (1:ℚ) with 1 /. 1; simp [h]
id                          └┘          
src     └─────┘ └┘ └───────┘└┘└┘  └────┘ └─
typ     └─────┘ └┘ └───────┘└┘└┘  └────┘└─
doc     └─────┘ └┘ └───────┘└┘└┘  └────┘ └─
txt     └─────┘ └┘ └───────┘  └┘  └────┘ └─
par     └─────┘ └┘ └───────┘  └┘  └────┘ └─
pid            └┘ └──────┘         
st     └───────────────────────────────────
372  
src  
typ  
doc  
txt  
par  
pid  
st   
373  protected theorem one_mul : 1 * a = a :=
id                                    
src                                   
typ                                   
374  num_denom_cases_on' a $ λ n d h,
id   └─────────────────┘        
src  └─────────────────┘
typ  └─────────────────┘        
375  by change (1:ℚ) with 1 /. 1; simp [h]
id                          └┘          
src     └─────┘ └┘ └───────┘└┘└┘  └────┘ └─
typ     └─────┘ └┘ └───────┘└┘└┘  └────┘└─
doc     └─────┘ └┘ └───────┘└┘└┘  └────┘ └─
txt     └─────┘ └┘ └───────┘  └┘  └────┘ └─
par     └─────┘ └┘ └───────┘  └┘  └────┘ └─
pid            └┘ └──────┘         
st     └───────────────────────────────────
376  
src  
typ  
doc  
txt  
par  
pid  
st   
377  protected theorem mul_comm : a * b = b * a :=
id                                      
src                                       
typ                                     
378  num_denom_cases_on' a $ λ n₁ d₁ h₁,
id   └─────────────────┘      └┘ └┘ └┘
src  └─────────────────┘
typ  └─────────────────┘      └┘ └┘ └┘
379  num_denom_cases_on' b $ λ n₂ d₂ h₂,
id   └─────────────────┘      └┘ └┘ └┘
src  └─────────────────┘
typ  └─────────────────┘      └┘ └┘ └┘
380  by simp [h₁, h₂, mul_comm]
id            └┘  └┘  └──────┘
src     └────┘  └┘  └┘└──────┘└─
typ     └────┘└┘└┘└┘└┘└──────┘└─
doc     └────┘  └┘  └┘        └─
txt     └────┘  └┘  └┘        └─
par     └────┘  └┘  └┘        └─
pid           └┘  └┘        
st     └────────────────────────
381  
src  
typ  
doc  
txt  
par  
pid  
st   
382  protected theorem mul_assoc : a * b * c = a * (b * c) :=
id                                            
src                                               
typ                                           
383  num_denom_cases_on' a $ λ n₁ d₁ h₁,
id   └─────────────────┘      └┘ └┘ └┘
src  └─────────────────┘
typ  └─────────────────┘      └┘ └┘ └┘
384  num_denom_cases_on' b $ λ n₂ d₂ h₂,
id   └─────────────────┘      └┘ └┘ └┘
src  └─────────────────┘
typ  └─────────────────┘      └┘ └┘ └┘
385  num_denom_cases_on' c $ λ n₃ d₃ h₃,
id   └─────────────────┘      └┘ └┘ └┘
src  └─────────────────┘
typ  └─────────────────┘      └┘ └┘ └┘
386  by simp [h₁, h₂, h₃, mul_ne_zero, mul_comm, mul_left_comm]
id            └┘  └┘  └┘  └─────────┘  └──────┘  └───────────┘
src     └────┘  └┘  └┘  └┘└─────────┘└┘└──────┘└┘└───────────┘└─
typ     └────┘└┘└┘└┘└┘└┘└┘└─────────┘└┘└──────┘└┘└───────────┘└─
doc     └────┘  └┘  └┘  └┘           └┘        └┘             └─
txt     └────┘  └┘  └┘  └┘           └┘        └┘             └─
par     └────┘  └┘  └┘  └┘           └┘        └┘             └─
pid           └┘  └┘  └┘           └┘        └┘             
st     └────────────────────────────────────────────────────────
387  
src  
typ  
doc  
txt  
par  
pid  
st   
388  protected theorem add_mul : (a + b) * c = a * c + b * c :=
id                                             
src                                                 
typ                                            
389  num_denom_cases_on' a $ λ n₁ d₁ h₁,
id   └─────────────────┘      └┘ └┘ └┘
src  └─────────────────┘
typ  └─────────────────┘      └┘ └┘ └┘
390  num_denom_cases_on' b $ λ n₂ d₂ h₂,
id   └─────────────────┘      └┘ └┘ └┘
src  └─────────────────┘
typ  └─────────────────┘      └┘ └┘ └┘
391  num_denom_cases_on' c $ λ n₃ d₃ h₃,
id   └─────────────────┘      └┘ └┘ └┘
src  └─────────────────┘
typ  └─────────────────┘      └┘ └┘ └┘
392  by simp [h₁, h₂, h₃, mul_ne_zero];
id            └┘  └┘  └┘  └─────────┘
src     └────┘  └┘  └┘  └┘└─────────┘
typ     └────┘└┘└┘└┘└┘└┘└┘└─────────┘
doc     └────┘  └┘  └┘  └┘           
txt     └────┘  └┘  └┘  └┘           
par     └────┘  └┘  └┘  └┘           
pid           └┘  └┘  └┘           
st     └────────────────────────────────
393     refine (div_mk_div_cancel_left (int.coe_nat_ne_zero.2 h₃)).symm.trans _;
id              └────────────────────┘  └─────────────────┘   └┘
src     └─────┘ └────────────────────┘ └─────────────────┘└─┘  └─────────────┘
typ     └─────┘ └────────────────────┘ └─────────────────┘└─┘└┘└─────────────┘
doc     └─────┘                                           └─┘  └─────────────┘
txt     └─────┘                                           └─┘  └─────────────┘
par     └─────┘                                           └─┘  └─────────────┘
pid                                                      └─┘  └─────────────┘
st   ────────────────────────────────────────────────────────────────────────────
394     simp [mul_add, mul_comm, mul_assoc, mul_left_comm]
id            └─────┘  └──────┘  └───────┘  └───────────┘
src     └────┘└─────┘└┘└──────┘└┘└───────┘└┘└───────────┘└─
typ     └────┘└─────┘└┘└──────┘└┘└───────┘└┘└───────────┘└─
doc     └────┘       └┘        └┘         └┘             └─
txt     └────┘       └┘        └┘         └┘             └─
par     └────┘       └┘        └┘         └┘             └─
pid                └┘        └┘         └┘             
st   ──────────────────────────────────────────────────────
395  
src  
typ  
doc  
txt  
par  
pid  
st   
396  protected theorem mul_add : a * (b + c) = a * b + a * c :=
id                                             
src                                                 
typ                                            
397  by rw [rat.mul_comm, rat.add_mul, rat.mul_comm, rat.mul_comm c a]
id          └──────────┘  └─────────┘  └──────────┘  └──────────┘  
src     └──┘└──────────┘└┘└─────────┘└┘└──────────┘└┘└──────────┘  └─
typ     └──┘└──────────┘└┘└─────────┘└┘└──────────┘└┘└──────────┘└─
doc     └──┘            └┘           └┘            └┘              └─
txt     └──┘            └┘           └┘            └┘              └─
par     └──┘            └┘           └┘            └┘              └─
pid       └┘            └┘           └┘            └┘              
st     └───────────────┘└───────────┘└────────────┘└────────────────┘
398  
src  
typ  
doc  
txt  
par  
pid  
st   
399  protected theorem zero_ne_one : 0 ≠ (1:ℚ) :=
id                                         
src                                        
typ                                        
doc                                         
400  mt (λ (h : 0 = 1 /. 1), (mk_eq_zero one_ne_zero).1 h.symm) one_ne_zero
id   └┘              └┘      └────────┘ └─────────┘   └───┘  └─────────┘
src  └┘              └┘      └────────┘ └─────────┘    └───┘  └─────────┘
typ  └┘              └┘      └────────┘ └─────────┘   └───┘  └─────────┘
doc                   └┘
401  
402  protected theorem mul_inv_cancel : a ≠ 0 → a * a⁻¹ = 1 :=
id                                              └┘ 
src                                                └┘ 
typ                                             └┘ 
403  num_denom_cases_on' a $ λ n d h a0,
id   └─────────────────┘         └┘
src  └─────────────────┘
typ  └─────────────────┘         └┘
404  have n0 : n ≠ 0, from mt (by intro e; subst e; simp) a0,
id                       └┘                            └┘
src                       └┘     └─────┘  └────┘   └──┘
typ                      └┘     └─────┘  └────┘  └──┘  └┘
doc                               └─────┘  └────┘   └──┘
txt                               └─────┘  └────┘   └──┘
par                               └─────┘  └────┘   └──┘
pid                                    └┘       
st                               └─────────────────────┘
405  by simp [h, n0, mul_comm]; exact
id              └┘  └──────┘
src     └────┘ └┘  └┘└──────┘  └────┘
typ     └────┘└┘└┘└┘└──────┘  └────┘
doc     └────┘ └┘  └┘          └────┘
txt     └────┘ └┘  └┘          └────┘
par     └────┘ └┘  └┘          └────┘
pid          └┘  └┘               
st     └──────────────────────────────
406  eq.trans (by simp) (@div_mk_div_cancel_left 1 1 _ n0)
id   └──────┘             └────────────────────┘       └┘
src  └──────┘   └──┘└┘  └────────────────────┘└─────┘  └─
typ  └──────┘   └──┘└┘  └────────────────────┘└─────┘└┘└─
doc             └──┘└┘                        └─────┘  └─
txt             └──┘└┘                        └─────┘  └─
par             └──┘└┘                        └─────┘  └─
pid             └─────┘                        └─────┘  
st   ───────────┘└───┘└────────────────────────────────────
407  
src  
typ  
doc  
txt  
par  
pid  
st   
408  protected theorem inv_mul_cancel (h : a ≠ 0) : a⁻¹ * a = 1 :=
id                                                └┘   
src                                                 └┘    
typ                                               └┘   
409  eq.trans (rat.mul_comm _ _) (rat.mul_inv_cancel _ h)
id   └──────┘  └──────────┘       └────────────────┘   
src  └──────┘  └──────────┘       └────────────────┘
typ  └──────┘  └──────────┘       └────────────────┘   
410  
411  instance : decidable_eq ℚ := by tactic.mk_dec_eq_instance
id              └──────────┘        └───────────────────────┘
src             └──────────┘        └───────────────────────┘
typ             └──────────┘        └───────────────────────┘
doc                          
par                                  └───────────────────────┘
st                                  └────────────────────────┘
412  
413  instance : discrete_field ℚ :=
id              └────────────┘ 
src             └────────────┘ 
typ             └────────────┘ 
doc                            
414  { zero             := 0,
415    add              := rat.add,
id                         └─────┘
src                        └─────┘
typ                        └─────┘
416    neg              := rat.neg,
id                         └─────┘
src                        └─────┘
typ                        └─────┘
417    one              := 1,
418    mul              := rat.mul,
id                         └─────┘
src                        └─────┘
typ                        └─────┘
419    inv              := rat.inv,
id                         └─────┘
src                        └─────┘
typ                        └─────┘
420    zero_add         := rat.zero_add,
id                         └──────────┘
src                        └──────────┘
typ                        └──────────┘
421    add_zero         := rat.add_zero,
id                         └──────────┘
src                        └──────────┘
typ                        └──────────┘
422    add_comm         := rat.add_comm,
id                         └──────────┘
src                        └──────────┘
typ                        └──────────┘
423    add_assoc        := rat.add_assoc,
id                         └───────────┘
src                        └───────────┘
typ                        └───────────┘
424    add_left_neg     := rat.add_left_neg,
id                         └──────────────┘
src                        └──────────────┘
typ                        └──────────────┘
425    mul_one          := rat.mul_one,
id                         └─────────┘
src                        └─────────┘
typ                        └─────────┘
426    one_mul          := rat.one_mul,
id                         └─────────┘
src                        └─────────┘
typ                        └─────────┘
427    mul_comm         := rat.mul_comm,
id                         └──────────┘
src                        └──────────┘
typ                        └──────────┘
428    mul_assoc        := rat.mul_assoc,
id                         └───────────┘
src                        └───────────┘
typ                        └───────────┘
429    left_distrib     := rat.mul_add,
id                         └─────────┘
src                        └─────────┘
typ                        └─────────┘
430    right_distrib    := rat.add_mul,
id                         └─────────┘
src                        └─────────┘
typ                        └─────────┘
431    zero_ne_one      := rat.zero_ne_one,
id                         └─────────────┘
src                        └─────────────┘
typ                        └─────────────┘
432    mul_inv_cancel   := rat.mul_inv_cancel,
id                         └────────────────┘
src                        └────────────────┘
typ                        └────────────────┘
433    inv_mul_cancel   := rat.inv_mul_cancel,
id                         └────────────────┘
src                        └────────────────┘
typ                        └────────────────┘
434    has_decidable_eq := rat.decidable_eq,
id                         └──────────────┘
src                        └──────────────┘
typ                        └──────────────┘
435    inv_zero         := rfl }
id                         └─┘
src                        └─┘
typ                        └─┘
436  
437  /- Extra instances to short-circuit type class resolution -/
438  instance : field ℚ              := by apply_instance
id              └───┘ 
src             └───┘                     └─────────────┘
typ             └───┘                     └─────────────┘
doc                                       └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
439  instance : division_ring ℚ      := by apply_instance
id              └───────────┘ 
src             └───────────┘             └─────────────┘
typ             └───────────┘             └─────────────┘
doc                                       └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
440  instance : integral_domain ℚ    := by apply_instance
id              └─────────────┘ 
src             └─────────────┘           └──────────────
typ             └─────────────┘           └──────────────
doc                                       └──────────────
txt                                        └──────────────
par                                        └──────────────
pid                                                      
st                                        └───────────────
441  -- TODO(Mario): this instance slows down data.real.basic
src  ─────────────────────────────────────────────────────────
typ  ─────────────────────────────────────────────────────────
doc  ─────────────────────────────────────────────────────────
txt  ─────────────────────────────────────────────────────────
par  ─────────────────────────────────────────────────────────
pid  ─────────────────────────────────────────────────────────
st   ─────────────────────────────────────────────────────────
442  --instance : domain ℚ           := by apply_instance
src  ────────────────────────────────────────────────────┘
typ  ────────────────────────────────────────────────────┘
doc  ────────────────────────────────────────────────────┘
txt  ────────────────────────────────────────────────────┘
par  ────────────────────────────────────────────────────┘
pid  ────────────────────────────────────────────────────┘
st   ────────────────────────────────────────────────────┘
443  instance : nonzero_comm_ring ℚ  := by apply_instance
id              └───────────────┘ 
src             └───────────────┘         └─────────────┘
typ             └───────────────┘         └─────────────┘
doc             └───────────────┘         └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
444  instance : comm_ring ℚ          := by apply_instance
id              └───────┘ 
src             └───────┘                 └──────────────
typ             └───────┘                 └──────────────
doc                                       └──────────────
txt                                        └──────────────
par                                        └──────────────
pid                                                      
st                                        └───────────────
445  --instance : ring ℚ             := by apply_instance
src  ────────────────────────────────────────────────────┘
typ  ────────────────────────────────────────────────────┘
doc  ────────────────────────────────────────────────────┘
txt  ────────────────────────────────────────────────────┘
par  ────────────────────────────────────────────────────┘
pid  ────────────────────────────────────────────────────┘
st   ────────────────────────────────────────────────────┘
446  instance : comm_semiring ℚ      := by apply_instance
id              └───────────┘ 
src             └───────────┘             └─────────────┘
typ             └───────────┘             └─────────────┘
doc                                       └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
447  instance : semiring ℚ           := by apply_instance
id              └──────┘ 
src             └──────┘                  └─────────────┘
typ             └──────┘                  └─────────────┘
doc                                       └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
448  instance : add_comm_group ℚ     := by apply_instance
id              └────────────┘ 
src             └────────────┘            └─────────────┘
typ             └────────────┘            └─────────────┘
doc                                       └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
449  instance : add_group ℚ          := by apply_instance
id              └───────┘ 
src             └───────┘                 └─────────────┘
typ             └───────┘                 └─────────────┘
doc                                       └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
450  instance : add_comm_monoid ℚ    := by apply_instance
id              └─────────────┘ 
src             └─────────────┘           └─────────────┘
typ             └─────────────┘           └─────────────┘
doc                                       └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
451  instance : add_monoid ℚ         := by apply_instance
id              └────────┘ 
src             └────────┘                └─────────────┘
typ             └────────┘                └─────────────┘
doc                                       └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
452  instance : add_left_cancel_semigroup ℚ := by apply_instance
id              └───────────────────────┘ 
src             └───────────────────────┘        └─────────────┘
typ             └───────────────────────┘        └─────────────┘
doc                                              └─────────────┘
txt                                               └─────────────┘
par                                               └─────────────┘
pid                                                             
st                                               └──────────────┘
453  instance : add_right_cancel_semigroup ℚ := by apply_instance
id              └────────────────────────┘ 
src             └────────────────────────┘        └─────────────┘
typ             └────────────────────────┘        └─────────────┘
doc                                               └─────────────┘
txt                                                └─────────────┘
par                                                └─────────────┘
pid                                                              
st                                                └──────────────┘
454  instance : add_comm_semigroup ℚ := by apply_instance
id              └────────────────┘ 
src             └────────────────┘        └─────────────┘
typ             └────────────────┘        └─────────────┘
doc                                       └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
455  instance : add_semigroup ℚ      := by apply_instance
id              └───────────┘ 
src             └───────────┘             └─────────────┘
typ             └───────────┘             └─────────────┘
doc                                       └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
456  instance : comm_monoid ℚ        := by apply_instance
id              └─────────┘ 
src             └─────────┘               └─────────────┘
typ             └─────────┘               └─────────────┘
doc                                       └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
457  instance : monoid ℚ             := by apply_instance
id              └────┘ 
src             └────┘                    └─────────────┘
typ             └────┘                    └─────────────┘
doc                                       └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
458  instance : comm_semigroup ℚ     := by apply_instance
id              └────────────┘ 
src             └────────────┘            └─────────────┘
typ             └────────────┘            └─────────────┘
doc                                       └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
459  instance : semigroup ℚ          := by apply_instance
id              └───────┘ 
src             └───────┘                 └──────────────
typ             └───────┘                 └──────────────
doc                                       └──────────────
txt                                        └──────────────
par                                        └──────────────
pid                                                      
st                                        └───────────────
460  
src  
typ  
doc  
txt  
par  
pid  
st   
461  theorem sub_def {a b c d : ℤ} (b0 : b ≠ 0) (d0 : d ≠ 0) :
id                                                  
src                                                   
typ                                                 
462    a /. b - c /. d = (a * d - c * b) /. (b * d) :=
id      └┘    └┘            └┘    
src      └┘      └┘                 └┘    
typ     └┘    └┘            └┘    
doc      └┘       └┘                     └┘
463  by simp [b0, d0]
id            └┘  └┘
src     └────┘  └┘  └─
typ     └────┘└┘└┘└┘└─
doc     └────┘  └┘  └─
txt     └────┘  └┘  └─
par     └────┘  └┘  └─
pid           └┘  
st     └──────────────
464  
src  
typ  
doc  
txt  
par  
pid  
st   
465  @[simp] lemma denom_neg_eq_denom : ∀ q : ℚ, (-q).denom = q.denom
id                                               └───┘   └────┘
src                                                └───┘    └────┘
typ                                              └───┘   └────┘
doc    └──┘                                   
466  | ⟨_, d, _, _⟩ := rfl
id                     └─┘
src                    └─┘
typ                    └─┘
467  
468  @[simp] lemma num_neg_eq_neg_num : ∀ q : ℚ, (-q).num = -(q.num)
id                                               └─┘    └──┘
src                                                └─┘     └──┘
typ                                              └─┘    └──┘
doc    └──┘                                   
469  | ⟨n, _, _, _⟩ := rfl
id                     └─┘
src                    └─┘
typ                    └─┘
470  
471  @[simp] lemma num_zero : rat.num 0 = 0 := rfl
id                            └─────┘         └─┘
src                           └─────┘         └─┘
typ                           └─────┘         └─┘
doc    └──┘
472  
473  lemma zero_of_num_zero {q : ℚ} (hq : q.num = 0) : q = 0 :=
id                                       └──┘        
src                                       └──┘         
typ                                      └──┘        
doc                              
474  have q = q.num /. q.denom, from num_denom.symm,
id          └──┘ └┘ └────┘       └───────┘└───┘
src           └──┘ └┘  └────┘       └───────┘└───┘
typ         └──┘ └┘ └────┘       └───────┘└───┘
doc                 └┘
475  by simpa [hq]
id             └┘
src     └─────┘  └─
typ     └─────┘└┘└─
doc     └─────┘  └─
txt     └─────┘  └─
par     └─────┘  └─
pid            
st     └───────────
476  
src  
typ  
doc  
txt  
par  
pid  
st   
477  lemma zero_iff_num_zero {q : ℚ} : q = 0 ↔ q.num = 0 :=
id                                         └──┘ 
src                                          └──┘ 
typ                                        └──┘ 
doc                               
478  ⟨λ _, by simp *, zero_of_num_zero⟩
id                   └──────────────┘
src           └────┘  └──────────────┘
typ          └────┘  └──────────────┘
doc           └────┘
txt           └────┘
par           └────┘
pid               
st           └─────┘
479  
480  lemma num_ne_zero_of_ne_zero {q : ℚ} (h : q ≠ 0) : q.num ≠ 0 :=
id                                                   └──┘ 
src                                                    └──┘ 
typ                                                  └──┘ 
doc                                    
481  assume : q.num = 0,
id            └──┘ 
src            └──┘ 
typ           └──┘ 
482  h $ zero_of_num_zero this
id      └──────────────┘ └──┘
src      └──────────────┘
typ     └──────────────┘ └──┘
483  
484  @[simp] lemma num_one : (1 : ℚ).num = 1 := rfl
id                                 └─┘        └─┘
src                                └─┘        └─┘
typ                                └─┘        └─┘
doc    └──┘                       
485  
486  @[simp] lemma denom_one : (1 : ℚ).denom = 1 := rfl
id                                   └───┘        └─┘
src                                  └───┘        └─┘
typ                                  └───┘        └─┘
doc    └──┘                         
487  
488  lemma denom_ne_zero (q : ℚ) : q.denom ≠ 0 :=
id                                └────┘ 
src                                └────┘ 
typ                               └────┘ 
doc                           
489  ne_of_gt q.pos
id   └──────┘ └──┘
src  └──────┘  └──┘
typ  └──────┘ └──┘
490  
491  lemma eq_iff_mul_eq_mul {p q : ℚ} : p = q ↔ p.num * q.denom = q.num * p.denom :=
id                                          └──┘  └────┘  └──┘  └────┘
src                                            └──┘   └────┘   └──┘   └────┘
typ                                         └──┘  └────┘  └──┘  └────┘
doc                                 
492  begin
st   └─────
493    conv_lhs { rw [←(@num_denom p), ←(@num_denom q)] },
id                       └───────┘       └───────┘ 
src    └─────────┘└───┘  └───────┘ └──┘  └───────┘ └─┘
typ    └─────────┘└───┘  └───────┘└──┘  └───────┘└─┘
txt    └─────────┘└───┘            └──┘            └─┘
par    └─────────┘└───┘            └──┘            └─┘
pid            └─────┘            └──┘            └──┘
st   ───────────┘└──────────────────┘└───────────────┘ └┘
494    exact rat.mk_eq (by exact_mod_cast p.denom_ne_zero) (by exact_mod_cast q.denom_ne_zero)
id           └───────┘                    └─────────────┘                     └─────────────┘
src    └────┘└───────┘   └─────────────┘└─────────────┘└┘   └─────────────┘└─────────────┘└┘
typ    └────┘└───────┘   └──────────────┘└─────────────┘└┘   └──────────────┘└─────────────┘└┘
doc    └────┘            └─────────────┘               └┘   └─────────────┘               └┘
txt    └────┘            └─────────────┘               └┘   └─────────────┘               └┘
par    └────┘            └──────────────┘               └┘   └──────────────┘               └┘
pid                     └──────────────┘               └┘   └──────────────┘               
st   ────────────────────┘└─────────────────────────────┘└───┘└─────────────────────────────┘└┘
495  end
st   └─┘
496  
497  lemma mk_num_ne_zero_of_ne_zero {q : ℚ} {n d : ℤ} (hq : q ≠ 0) (hqnd : q = n /. d) : n ≠ 0 :=
id                                                                         └┘      
src                                                                           └┘        
typ                                                                        └┘      
doc                                                                              └┘
498  assume : n = 0,
id             
src             
typ            
499  hq $ by simpa [this] using hqnd
id   └┘             └──┘        └──┘
src          └─────┘    └──────┘    
typ  └┘      └─────┘└──┘└──────┘└──┘
doc          └─────┘    └──────┘    
txt          └─────┘    └──────┘    
par          └─────┘    └──────┘    
pid                   └────┘    
st          └────────────────────────
500  
src  
typ  
doc  
txt  
par  
pid  
st   
501  lemma mk_denom_ne_zero_of_ne_zero {q : ℚ} {n d : ℤ} (hq : q ≠ 0) (hqnd : q = n /. d) : d ≠ 0 :=
id                                                                           └┘      
src                                                                             └┘        
typ                                                                          └┘      
doc                                                                                └┘
502  assume : d = 0,
id             
src             
typ            
503  hq $ by simpa [this] using hqnd
id   └┘             └──┘        └──┘
src          └─────┘    └──────┘    
typ  └┘      └─────┘└──┘└──────┘└──┘
doc          └─────┘    └──────┘    
txt          └─────┘    └──────┘    
par          └─────┘    └──────┘    
pid                   └────┘    
st          └────────────────────────
504  
src  
typ  
doc  
txt  
par  
pid  
st   
505  lemma mk_ne_zero_of_ne_zero {n d : ℤ} (h : n ≠ 0) (hd : d ≠ 0) : n /. d ≠ 0 :=
id                                                                └┘  
src                                                                  └┘   
typ                                                               └┘  
doc                                                                     └┘
506  assume : n /. d = 0,
id             └┘  
src             └┘   
typ            └┘  
doc             └┘
507  h $ (mk_eq_zero hd).1 this
id       └────────┘ └┘   └──┘
src       └────────┘    
typ      └────────┘ └┘   └──┘
508  
509  lemma mul_num_denom (q r : ℚ) : q * r = (q.num * r.num) /. ↑(q.denom * r.denom) :=
id                                       └──┘  └──┘  └┘  └────┘  └────┘
src                                         └──┘   └──┘  └┘   └────┘   └────┘
typ                                      └──┘  └──┘  └┘  └────┘  └────┘
doc                                                         └┘
510  have hq' : (↑q.denom : ℤ) ≠ 0, by have := denom_ne_zero q; simpa,
id               └────┘                    └───────────┘ 
src               └────┘            └──────┘└───────────┘   └───┘
typ              └────┘            └──────┘└───────────┘  └───┘
doc                                    └──────┘                └───┘
txt                                    └──────┘                └───┘
par                                    └──────┘                └───┘
pid                                    └───┘└─┘             
st                                    └─────────────────────────────┘
511  have hr' : (↑r.denom : ℤ) ≠ 0, by have := denom_ne_zero r; simpa,
id               └────┘                    └───────────┘ 
src               └────┘            └──────┘└───────────┘   └───┘
typ              └────┘            └──────┘└───────────┘  └───┘
doc                                    └──────┘                └───┘
txt                                    └──────┘                └───┘
par                                    └──────┘                └───┘
pid                                    └───┘└─┘             
st                                    └─────────────────────────────┘
512  suffices (q.num /. ↑q.denom) * (r.num /. ↑r.denom) = (q.num * r.num) /. ↑(q.denom * r.denom),
id             └──┘ └┘ └────┘    └──┘ └┘ └────┘    └──┘  └──┘  └┘  └────┘  └────┘
src             └──┘ └┘  └────┘     └──┘ └┘  └────┘     └──┘   └──┘  └┘   └────┘   └────┘
typ            └──┘ └┘ └────┘    └──┘ └┘ └────┘    └──┘  └──┘  └┘  └────┘  └────┘
doc                  └┘                    └┘                             └┘
513    by simpa using this,
id                    └──┘
src       └──────────┘
typ       └──────────┘└──┘
doc       └──────────┘
txt       └──────────┘
par       └──────────┘
pid            └────┘
st       └───────────────┘
514  by simp [mul_def hq' hr', -num_denom]
id            └─────┘ └─┘ └─┘
src     └────┘└─────┘      └─────────────
typ     └────┘└─────┘└─┘└─┘└─────────────
doc     └────┘             └─────────────
txt     └────┘             └─────────────
par     └────┘             └─────────────
pid                      └───────────┘
st     └───────────────────────────────────
515  
src  
typ  
doc  
txt  
par  
pid  
st   
516  lemma div_num_denom (q r : ℚ) : q / r = (q.num * r.denom) /. (q.denom * r.num) :=
id                                       └──┘  └────┘  └┘  └────┘  └──┘
src                                         └──┘   └────┘  └┘   └────┘   └──┘
typ                                      └──┘  └────┘  └┘  └────┘  └──┘
doc                                                           └┘
517  if hr : r.num = 0 then
id   └┘      └──┘ 
src  └┘       └──┘ 
typ  └┘      └──┘ 
518    have hr' : r = 0, from zero_of_num_zero hr,
id                          └──────────────┘ └┘
src                          └──────────────┘
typ                         └──────────────┘ └┘
519    by simp *
src       └─────┘
typ       └─────┘
doc       └─────┘
txt       └─────┘
par       └─────┘
pid           
st       └──────┘
520  else calc q / r = q * r⁻¹ : div_eq_mul_inv
id                    └┘   └────────────┘
src                       └┘   └────────────┘
typ                   └┘   └────────────┘
521              ... = (q.num /. q.denom) * (r.num /. r.denom)⁻¹ : by simp
id                      └──┘ └┘ └────┘    └──┘ └┘ └────┘ └┘
src                      └──┘ └┘  └────┘     └──┘ └┘  └────┘ └┘      └────
typ                     └──┘ └┘ └────┘    └──┘ └┘ └────┘ └┘      └────
doc                           └┘                   └┘                 └────
txt                                                                   └────
par                                                                   └────
pid                                                                       
st                                                                   └─────
522              ... = (q.num /. q.denom) * (r.denom /. r.num) : by rw inv_def
id                      └──┘ └┘ └────┘    └────┘ └┘ └──┘          └─────┘
src  ───────────┘        └──┘ └┘  └────┘     └────┘ └┘  └──┘       └─┘└─────┘
typ  ───────────┘       └──┘ └┘ └────┘    └────┘ └┘ └──┘       └─┘└─────┘
doc  ───────────┘             └┘                     └┘             └─┘       
txt  ───────────┘                                                   └─┘       
par  ───────────┘                                                   └─┘       
pid  ───────────┘                                                            
st   ───────────┘                                                  └───────────
523              ... = (q.num * r.denom) /. (q.denom * r.num) : mul_def (by simpa using denom_ne_zero q) hr
id               └─┘    └──┘  └────┘  └┘  └────┘  └──┘    └─────┘                 └───────────┘   └┘
src  ───────────┘        └──┘   └────┘  └┘   └────┘   └──┘    └─────┘     └──────────┘└───────────┘
typ  ───────────┘└─┘    └──┘  └────┘  └┘  └────┘  └──┘    └─────┘     └──────────┘└───────────┘  └┘
doc  ───────────┘                        └┘                                 └──────────┘             
txt  ───────────┘                                                           └──────────┘             
par  ───────────┘                                                           └──────────┘             
pid  ───────────┘                                                                └────┘             
st   ───────────┘                                                          └──────────────────────────┘
524  
525  lemma num_denom_mk {q : ℚ} {n d : ℤ} (hn : n ≠ 0) (hd : d ≠ 0) (qdf : q = n /. d) :
id                                                                      └┘ 
src                                                                         └┘
typ                                                                     └┘ 
doc                                                                             └┘
526        ∃ c : ℤ, n = c * q.num ∧ d = c * q.denom :=
id                   └──┘      └────┘
src                     └──┘         └────┘
typ                  └──┘      └────┘
527  have hq : q ≠ 0, from
id              
src              
typ             
528    assume : q = 0,
id               
src               
typ              
529    hn $ (rat.mk_eq_zero hd).1 (by cc),
id     └┘    └────────────┘ └┘ 
src          └────────────┘          └┘
typ    └┘    └────────────┘ └┘       └┘
doc                                   └┘
txt                                   └┘
par                                   └┘
st                                   └─┘
530  have q.num /. q.denom = n /. d, by rwa [num_denom],
id        └──┘ └┘ └────┘   └┘           └───────┘
src        └──┘ └┘  └────┘    └┘       └───┘└───────┘
typ       └──┘ └┘ └────┘   └┘      └───┘└───────┘
doc             └┘             └┘       └───┘         
txt                                     └───┘         
par                                     └───┘         
pid                                        └┘         
st                                     └─────────────┘
531  have q.num * d = n * ↑(q.denom), from (rat.mk_eq (by simp [rat.denom_ne_zero]) hd).1 this,
id        └──┘       └────┘         └───────┘           └───────────────┘   └┘   └──┘
src        └──┘          └────┘         └───────┘     └────┘└───────────────┘     
typ       └──┘       └────┘         └───────┘     └────┘└───────────────┘  └┘   └──┘
doc                                                       └────┘                 
txt                                                       └────┘                 
par                                                       └────┘                 
pid                                                                            
st                                                       └───────────────────────┘
532  begin
st   └─────
533    existsi n / q.num,
id               └───┘
src    └──────┘ └───┘
typ    └──────┘└───┘
doc    └──────┘  
txt    └──────┘  
par    └──────┘  
pid             
st   ──────────────────┘└─
534    have hqdn : q.num ∣ n, begin rw qdf, apply rat.num_dvd, assumption end,
id                 └───┘             └─┘        └─────────┘
src    └──────────┘└───┘         └─┘     └────┘└─────────┘  └─────────┘
typ    └──────────┘└───┘        └─┘└─┘  └────┘└─────────┘  └─────────┘
doc    └──────────┘               └─┘     └────┘             └─────────┘
txt    └──────────┘               └─┘     └────┘             └─────────┘
par    └──────────┘               └─┘     └────┘             └─────────┘
pid    └───────┘└─┘                                                  
st   ──────────────────────┘└─────┘└─────┘└─────────────────┘└───────────┘└─┘└─
535    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
536      { rw int.div_mul_cancel hqdn },
id            └────────────────┘ └──┘
src        └─┘└────────────────┘    
typ        └─┘└────────────────┘└──┘
doc        └─┘                      
txt        └─┘                      
par        └─┘                      
pid                                
st   ─────┘└─────────────────────────┘└┘
537      { apply int.eq_mul_div_of_mul_eq_mul_of_dvd_left,
id               └──────────────────────────────────────┘
src        └────┘└──────────────────────────────────────┘
typ        └────┘└──────────────────────────────────────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ───────────────────────────────────────────────────┘└─
538        {apply rat.num_ne_zero_of_ne_zero hq},
id                └────────────────────────┘ └┘
src         └────┘└────────────────────────┘
typ         └────┘└────────────────────────┘└┘
doc         └────┘                          
txt         └────┘                          
par         └────┘                          
pid                                        
st   ─────────────────────────────────────────┘└┘
539        {simp [rat.denom_ne_zero]},
id                └───────────────┘
src         └────┘└───────────────┘
typ         └────┘└───────────────┘
doc         └────┘                 
txt         └────┘                 
par         └────┘                 
pid                              
st   ──────────────────────────────┘└┘
540        repeat {assumption} }
src        └──────┘└────────┘└┘
typ        └──────┘└────────┘└┘
doc        └──────┘└────────┘└┘
txt        └──────┘└────────┘└┘
par        └──────┘└────────┘└┘
pid              └───────────┘
st   ─────────────┘└────────┘└─
541  end
st   ──┘
542  
543  theorem mk_pnat_num (n : ℤ) (d : ℕ+) :
id                                   └┘
src                                  └┘
typ                                  └┘
doc                                   └┘
544    (mk_pnat n d).num = n / nat.gcd n.nat_abs d :=
id      └─────┘   └─┘     └─────┘ └──────┘ 
src     └─────┘     └─┘      └─────┘  └──────┘
typ     └─────┘   └─┘     └─────┘ └──────┘ 
doc     └─────┘
545  by cases d; refl
id            
src     └────┘   └────
typ     └────┘  └────
doc     └────┘   └────
txt     └────┘   └────
par     └────┘   └────
pid                 
st     └──────────────
546  
src  
typ  
doc  
txt  
par  
pid  
st   
547  theorem mk_pnat_denom (n : ℤ) (d : ℕ+) :
id                                     └┘
src                                    └┘
typ                                    └┘
doc                                     └┘
548    (mk_pnat n d).denom = d / nat.gcd n.nat_abs d :=
id      └─────┘   └───┘     └─────┘ └──────┘ 
src     └─────┘     └───┘      └─────┘  └──────┘
typ     └─────┘   └───┘     └─────┘ └──────┘ 
doc     └─────┘
549  by cases d; refl
id            
src     └────┘   └────
typ     └────┘  └────
doc     └────┘   └────
txt     └────┘   └────
par     └────┘   └────
pid                 
st     └──────────────
550  
src  
typ  
doc  
txt  
par  
pid  
st   
551  theorem mul_num (q₁ q₂ : ℚ) : (q₁ * q₂).num =
id                                 └┘  └┘ └─┘  
src                                       └─┘  
typ                                └┘  └┘ └─┘  
doc                           
552    (q₁.num * q₂.num) / nat.gcd (q₁.num * q₂.num).nat_abs (q₁.denom * q₂.denom) :=
id      └┘└──┘  └┘└──┘   └─────┘  └┘└──┘  └┘└──┘ └─────┘   └┘└────┘  └┘└────┘
src       └──┘    └──┘   └─────┘    └──┘    └──┘ └─────┘     └────┘    └────┘
typ     └┘└──┘  └┘└──┘   └─────┘  └┘└──┘  └┘└──┘ └─────┘   └┘└────┘  └┘└────┘
553  by cases q₁; cases q₂; refl
id            └┘        └┘
src     └────┘    └────┘    └────
typ     └────┘└┘  └────┘└┘  └────
doc     └────┘    └────┘    └────
txt     └────┘    └────┘    └────
par     └────┘    └────┘    └────
pid                           
st     └─────────────────────────
554  
src  
typ  
doc  
txt  
par  
pid  
st   
555  theorem mul_denom (q₁ q₂ : ℚ) : (q₁ * q₂).denom =
id                                   └┘  └┘ └───┘  
src                                         └───┘  
typ                                  └┘  └┘ └───┘  
doc                             
556    (q₁.denom * q₂.denom) / nat.gcd (q₁.num * q₂.num).nat_abs (q₁.denom * q₂.denom) :=
id      └┘└────┘  └┘└────┘   └─────┘  └┘└──┘  └┘└──┘ └─────┘   └┘└────┘  └┘└────┘
src       └────┘    └────┘   └─────┘    └──┘    └──┘ └─────┘     └────┘    └────┘
typ     └┘└────┘  └┘└────┘   └─────┘  └┘└──┘  └┘└──┘ └─────┘   └┘└────┘  └┘└────┘
557  by cases q₁; cases q₂; refl
id            └┘        └┘
src     └────┘    └────┘    └────
typ     └────┘└┘  └────┘└┘  └────
doc     └────┘    └────┘    └────
txt     └────┘    └────┘    └────
par     └────┘    └────┘    └────
pid                           
st     └─────────────────────────
558  
src  
typ  
doc  
txt  
par  
pid  
st   
559  theorem mul_self_num (q : ℚ) : (q * q).num = q.num * q.num :=
id                                     └─┘   └──┘  └──┘
src                                      └─┘    └──┘   └──┘
typ                                    └─┘   └──┘  └──┘
doc                            
560  by rw [mul_num, int.nat_abs_mul, nat.coprime.gcd_eq_one, int.coe_nat_one, int.div_one];
id          └─────┘  └─────────────┘  └────────────────────┘  └─────────────┘  └─────────┘
src     └──┘└─────┘└┘└─────────────┘└┘└────────────────────┘└┘└─────────────┘└┘└─────────┘
typ     └──┘└─────┘└┘└─────────────┘└┘└────────────────────┘└┘└─────────────┘└┘└─────────┘
doc     └──┘       └┘               └┘                      └┘               └┘           
txt     └──┘       └┘               └┘                      └┘               └┘           
par     └──┘       └┘               └┘                      └┘               └┘           
pid       └┘       └┘               └┘                      └┘               └┘           
st     └──────────┘└───────────────┘└──────────────────────┘└───────────────┘└───────────┘└─
561  exact (q.cop.mul_right q.cop).mul (q.cop.mul_right q.cop)
id                                      └─────────────┘ └───┘
src  └────┘                     └────┘ └─────────────┘└───┘└─
typ  └────┘                     └────┘ └─────────────┘└───┘└─
doc  └────┘                     └────┘                     └─
txt  └────┘                     └────┘                     └─
par  └────┘                     └────┘                     └─
pid                            └────┘                     
st   ──────────────────────────────────────────────────────────
562  
src  
typ  
doc  
txt  
par  
pid  
st   
563  theorem mul_self_denom (q : ℚ) : (q * q).denom = q.denom * q.denom :=
id                                       └───┘   └────┘  └────┘
src                                        └───┘    └────┘   └────┘
typ                                      └───┘   └────┘  └────┘
doc                              
564  by rw [rat.mul_denom, int.nat_abs_mul, nat.coprime.gcd_eq_one, nat.div_one];
id          └───────────┘  └─────────────┘  └────────────────────┘  └─────────┘
src     └──┘└───────────┘└┘└─────────────┘└┘└────────────────────┘└┘└─────────┘
typ     └──┘└───────────┘└┘└─────────────┘└┘└────────────────────┘└┘└─────────┘
doc     └──┘             └┘               └┘                      └┘           
txt     └──┘             └┘               └┘                      └┘           
par     └──┘             └┘               └┘                      └┘           
pid       └┘             └┘               └┘                      └┘           
st     └────────────────┘└───────────────┘└──────────────────────┘└───────────┘└─
565  exact (q.cop.mul_right q.cop).mul (q.cop.mul_right q.cop)
id                                      └─────────────┘ └───┘
src  └────┘                     └────┘ └─────────────┘└───┘└─
typ  └────┘                     └────┘ └─────────────┘└───┘└─
doc  └────┘                     └────┘                     └─
txt  └────┘                     └────┘                     └─
par  └────┘                     └────┘                     └─
pid                            └────┘                     
st   ──────────────────────────────────────────────────────────
566  
src  
typ  
doc  
txt  
par  
pid  
st   
567  lemma add_num_denom (q r : ℚ) : q + r =
id                                     
src                                      
typ                                    
doc                             
568    ((q.num * r.denom + q.denom * r.num : ℤ)) /. (↑q.denom * ↑r.denom : ℤ) :=
id       └──┘  └────┘  └────┘  └──┘      └┘  └────┘  └────┘   
src       └──┘   └────┘   └────┘   └──┘      └┘   └────┘   └────┘   
typ      └──┘  └────┘  └────┘  └──┘      └┘  └────┘  └────┘   
doc                                              └┘
569  have hqd : (q.denom : ℤ) ≠ 0, from int.coe_nat_ne_zero_iff_pos.2 q.3,
id               └────┘              └─────────────────────────┘  
src               └────┘              └─────────────────────────┘   
typ              └────┘              └─────────────────────────┘  
570  have hrd : (r.denom : ℤ) ≠ 0, from int.coe_nat_ne_zero_iff_pos.2 r.3,
id               └────┘              └─────────────────────────┘  
src               └────┘              └─────────────────────────┘   
typ              └────┘              └─────────────────────────┘  
571  by conv_lhs { rw [←@num_denom q, ←@num_denom r, rat.add_def hqd hrd] };
id                       └───────┘     └───────┘   └─────────┘ └─┘ └─┘
src     └─────────┘└───┘ └───────┘ └─┘ └───────┘ └┘└─────────┘      └┘
typ     └─────────┘└───┘ └───────┘└─┘ └───────┘└┘└─────────┘└─┘└─┘└┘
txt     └─────────┘└───┘           └─┘           └┘                 └┘
par     └─────────┘└───┘           └─┘           └┘                 └┘
pid             └─────┘           └─┘           └┘                 └─┘
st     └─────────┘└────────────────┘└─────────────┘└───────────────────┘ └┘
572    simp [mul_comm]
id           └──────┘
src    └────┘└──────┘└─
typ    └────┘└──────┘└─
doc    └────┘        └─
txt    └────┘        └─
par    └────┘        └─
pid                
st   ──────────────────
573  
src  
typ  
doc  
txt  
par  
pid  
st   
574  section casts
575  
576  theorem coe_int_eq_mk : ∀ (z : ℤ), ↑z = z /. 1
id                                       └┘
src                                         └┘
typ                                      └┘
doc                                            └┘
577  | (n : ℕ) := show (n:ℚ) = n /. 1,
id                           └┘
src                           └┘
typ                          └┘
doc                             └┘
578    by induction n with n IH n; simp [*, show (1:ℚ) = 1 /. 1, from rfl]
id                                                                  └─┘
src       └────────┘ └──────────┘  └───────┘     └┘ └┘└─┘  └───────┘└─┘└┘
typ       └────────┘└──────────┘  └───────┘     └┘ └┘└─┘  └───────┘└─┘└┘
doc       └────────┘ └──────────┘  └───────┘     └┘ └┘ └─┘  └───────┘   └┘
txt       └────────┘ └──────────┘  └───────┘     └┘ └┘ └─┘  └───────┘   └┘
par       └────────┘ └──────────┘  └───────┘     └┘ └┘ └─┘  └───────┘   └┘
pid                 └─────────┘      └──┘     └┘ └┘ └─┘  └───────┘   
st       └────────────────────────────────────────────────────────────────┘
579  | -[1+ n] := show (-(n + 1) : ℚ) = -[1+ n] /. 1, begin
id     └──┘                       └──┘   └┘
src    └──┘                        └──┘   └┘
typ    └──┘                       └──┘   └┘
doc                                            └┘
st                                                    └─────
580    induction n with n IH, {refl},
id               
src    └────────┘ └────────┘   └──┘
typ    └────────┘└────────┘   └──┘
doc    └────────┘ └────────┘   └──┘
txt    └────────┘ └────────┘   └──┘
par    └────────┘ └────────┘   └──┘
pid              └───────┘
st   ──────────────────────┘└─────┘└┘
581    show -(n + 1 + 1 : ℚ) = -[1+ n.succ] /. 1,
id                                └────┘
src    └───┘  └─┘ └───┘ └┘     └────┘   └┘
typ    └───┘  └─┘ └───┘ └┘     └────┘   └┘
doc    └───┘    └─┘ └───┘ └┘              └┘
txt    └───┘    └─┘ └───┘ └┘              └┘
par    └───┘    └─┘ └───┘ └┘              └┘
pid    └───┘    └─┘ └───┘ └┘              
st   ──────────────────────────────────────────┘└─
582    rw [neg_add, IH],
id         └─────┘  └┘
src    └──┘└─────┘└┘  
typ    └──┘└─────┘└┘└┘
doc    └──┘       └┘  
txt    └──┘       └┘  
par    └──┘       └┘  
pid      └┘       └┘  
st   ────────────┘└──┘└──
583    simpa [show -1 = (-1) /. 1, from rfl]
id                                     └─┘
src    └─────┘     └┘   └─┘  └───────┘└─┘└┘
typ    └─────┘     └┘  └─┘  └───────┘└─┘└┘
doc    └─────┘     └┘   └─┘  └───────┘   └┘
txt    └─────┘     └┘   └─┘  └───────┘   └┘
par    └─────┘     └┘   └─┘  └───────┘   └┘
pid              └┘   └─┘  └───────┘   
st   ───────────────────────────────────────┘
584  end
st   └─┘
585  
586  theorem mk_eq_div (n d : ℤ) : n /. d = ((n : ℚ) / d) :=
id                                 └┘           
src                                 └┘            
typ                                └┘           
doc                                  └┘           
587  begin
st   └─────
588    by_cases d0 : d = 0, {simp [d0, div_zero]},
id                               └┘  └──────┘
src    └───────┘  └─┘ └┘   └────┘  └┘└──────┘
typ    └───────┘  └─┘└┘   └────┘└┘└┘└──────┘
doc    └───────┘  └─┘  └┘   └────┘  └┘        
txt    └───────┘  └─┘  └┘   └────┘  └┘        
par    └───────┘  └─┘  └┘   └────┘  └┘        
pid              └─┘           └┘        
st   ────────────────────┘└────────────────────┘└┘
589    simp [division_def, coe_int_eq_mk, mul_def one_ne_zero d0]
id           └──────────┘  └───────────┘  └─────┘ └─────────┘ └┘
src    └────┘└──────────┘└┘└───────────┘└┘└─────┘└─────────┘  └┘
typ    └────┘└──────────┘└┘└───────────┘└┘└─────┘└─────────┘└┘└┘
doc    └────┘            └┘             └┘                    └┘
txt    └────┘            └┘             └┘                    └┘
par    └────┘            └┘             └┘                    └┘
pid                    └┘             └┘                    
st   ────────────────────────────────────────────────────────────┘
590  end
st   └─┘
591  
592  theorem coe_int_eq_of_int (z : ℤ) : ↑z = of_int z :=
id                                        └────┘ 
src                                        └────┘
typ                                       └────┘ 
doc                                           └────┘
593  (coe_int_eq_mk z).trans (of_int_eq_mk z).symm
id    └───────────┘  └───┘   └──────────┘  └──┘
src   └───────────┘   └───┘   └──────────┘   └──┘
typ   └───────────┘  └───┘   └──────────┘  └──┘
594  
595  @[simp, elim_cast] theorem coe_int_num (n : ℤ) : (n : ℚ).num = n :=
id                                                        └─┘   
src                                                        └─┘  
typ                                                       └─┘   
doc    └──┘  └───────┘                                     
596  by rw coe_int_eq_of_int; refl
id         └───────────────┘
src     └─┘└───────────────┘  └────
typ     └─┘└───────────────┘  └────
doc     └─┘                   └────
txt     └─┘                   └────
par     └─┘                   └────
pid                              
st     └───────────────────────────
597  
src  
typ  
doc  
txt  
par  
pid  
st   
598  @[simp, elim_cast] theorem coe_int_denom (n : ℤ) : (n : ℚ).denom = 1 :=
id                                                          └───┘  
src                                                          └───┘  
typ                                                         └───┘  
doc    └──┘  └───────┘                                       
599  by rw coe_int_eq_of_int; refl
id         └───────────────┘
src     └─┘└───────────────┘  └────
typ     └─┘└───────────────┘  └────
doc     └─┘                   └────
txt     └─┘                   └────
par     └─┘                   └────
pid                              
st     └───────────────────────────
600  
src  
typ  
doc  
txt  
par  
pid  
st   
601  lemma coe_int_num_of_denom_eq_one {q : ℚ} (hq : q.denom = 1) : ↑(q.num) = q :=
id                                                  └────┘        └──┘   
src                                                  └────┘         └──┘  
typ                                                 └────┘        └──┘   
doc                                         
602  by { conv_rhs { rw [←(@num_denom q), hq] }, rw [coe_int_eq_mk], refl }
id                          └───────┘    └┘         └───────────┘
src       └─────────┘└───┘  └───────┘ └─┘  └┘  └──┘└───────────┘  └───┘
typ       └─────────┘└───┘  └───────┘└─┘└┘└┘  └──┘└───────────┘  └───┘
doc                                              └──┘               └───┘
txt       └─────────┘└───┘            └─┘  └┘  └──┘               └───┘
par       └─────────┘└───┘            └─┘  └┘  └──┘               └───┘
pid               └─────┘            └─┘  └─┘    └┘                   
st     └───────────┘└──────────────────┘└──┘ └┘└────────────────┘└──────┘└┘
603  
604  instance : can_lift ℚ ℤ :=
id              └──────┘  
src             └──────┘  
typ             └──────┘  
doc             └──────┘ 
605  ⟨coe, λ q, q.denom = 1, λ q hq, ⟨q.num, coe_int_num_of_denom_eq_one hq⟩⟩
id    └─┘      └────┘        └┘   └──┘  └─────────────────────────┘ └┘
src   └─┘        └────┘               └──┘  └─────────────────────────┘
typ   └─┘      └────┘        └┘   └──┘  └─────────────────────────┘ └┘
606  
607  theorem coe_nat_eq_mk (n : ℕ) : ↑n = n /. 1 :=
id                                     └┘
src                                      └┘
typ                                    └┘
doc                                         └┘
608  by rw [← int.cast_coe_nat, coe_int_eq_mk]
id            └──────────────┘  └───────────┘
src     └────┘└──────────────┘└┘└───────────┘└─
typ     └────┘└──────────────┘└┘└───────────┘└─
doc     └────┘                └┘             └─
txt     └────┘                └┘             └─
par     └────┘                └┘             └─
pid       └──┘                └┘             
st     └─────────────────────┘└─────────────┘
609  
src  
typ  
doc  
txt  
par  
pid  
st   
610  @[simp, elim_cast] theorem coe_nat_num (n : ℕ) : (n : ℚ).num = n :=
id                                                        └─┘   
src                                                        └─┘  
typ                                                       └─┘   
doc    └──┘  └───────┘                                     
611  by rw [← int.cast_coe_nat, coe_int_num]
id            └──────────────┘  └─────────┘
src     └────┘└──────────────┘└┘└─────────┘└─
typ     └────┘└──────────────┘└┘└─────────┘└─
doc     └────┘                └┘           └─
txt     └────┘                └┘           └─
par     └────┘                └┘           └─
pid       └──┘                └┘           
st     └─────────────────────┘└───────────┘
612  
src  
typ  
doc  
txt  
par  
pid  
st   
613  @[simp, elim_cast] theorem coe_nat_denom (n : ℕ) : (n : ℚ).denom = 1 :=
id                                                          └───┘  
src                                                          └───┘  
typ                                                         └───┘  
doc    └──┘  └───────┘                                       
614  by rw [← int.cast_coe_nat, coe_int_denom]
id            └──────────────┘  └───────────┘
src     └────┘└──────────────┘└┘└───────────┘└─
typ     └────┘└──────────────┘└┘└───────────┘└─
doc     └────┘                └┘             └─
txt     └────┘                └┘             └─
par     └────┘                └┘             └─
pid       └──┘                └┘             
st     └─────────────────────┘└─────────────┘
615  
src  
typ  
doc  
txt  
par  
pid  
st   
616  end casts
617  
618  lemma inv_def' {q : ℚ} : q⁻¹ = (q.denom : ℚ) / q.num :=
id                           └┘   └────┘      └──┘
src                           └┘    └────┘       └──┘
typ                          └┘   └────┘      └──┘
doc                                           
619  by { conv_lhs { rw ←(@num_denom q) }, cases q, simp [div_num_denom] }
id                         └───────┘                    └───────────┘
src       └─────────┘└──┘  └───────┘ └┘  └────┘   └────┘└───────────┘└┘
typ       └─────────┘└──┘  └───────┘└┘  └────┘  └────┘└───────────┘└┘
doc                                        └────┘   └────┘             └┘
txt       └─────────┘└──┘            └┘  └────┘   └────┘             └┘
par       └─────────┘└──┘            └┘  └────┘   └────┘             └┘
pid               └────┘            └─┘                           
st     └───────────┘└──────────────────┘└┘└──────┘└─────────────────────┘└┘
620  
621  @[simp] lemma mul_own_denom_eq_num {q : ℚ} : q * q.denom = q.num :=
id                                                 └────┘  └──┘
src                                                  └────┘   └──┘
typ                                                └────┘  └──┘
doc    └──┘                                  
622  begin
st   └─────
623    suffices : mk (q.num) ↑(q.denom) * mk ↑(q.denom) 1 = mk (q.num) 1, by
id                                           └─────┘     └┘  └───┘
src    └─────────┘        └┘        └┘    └─────┘└──┘└┘ └───┘└─┘
typ    └─────────┘        └┘        └┘    └─────┘└──┘└┘ └───┘└─┘
doc    └─────────┘        └┘         └┘            └──┘ └┘      └─┘
txt    └─────────┘        └┘         └┘            └──┘         └─┘
par    └─────────┘        └┘         └┘            └──┘         └─┘
pid    └───────┘└┘        └┘         └┘            └──┘         └┘
st   ──────────────────────────────────────────────────────────────────┘
624    { conv { for q [1] { rw ←(@num_denom q) }}, rwa [coe_int_eq_mk, coe_nat_eq_mk] },
id                               └───────┘            └───────────┘  └───────────┘
src      └─────┘└──┘ └─────┘└──┘  └───────┘ └┘  └───┘└───────────┘└┘└───────────┘└┘
typ      └─────┘└──┘└─────┘└──┘  └───────┘└┘  └───┘└───────────┘└┘└───────────┘└┘
doc                                                └───┘             └┘             └┘
txt      └─────┘└──┘ └─────┘└──┘            └┘  └───┘             └┘             └┘
par      └─────┘└──┘ └─────┘└──┘            └┘  └───┘             └┘             └┘
pid          └────┘ └─────────┘            └──┘     └┘             └┘             
st     └─────┘└──────────┘└──────────────────┘└┘└─────────────────┘└─────────────┘└┘
625    have : (q.denom : ℤ) ≠ 0, from ne_of_gt (by exact_mod_cast q.pos),
id             └─────┘               └──────┘                    └───┘
src    └─────┘ └─────┘└─┘ └┘└┘  └───┘└──────┘   └─────────────┘└───┘
typ    └─────┘ └─────┘└─┘ └┘└┘  └───┘└──────┘   └──────────────┘└───┘
doc    └─────┘        └─┘ └┘ └┘  └───┘           └─────────────┘     
txt    └─────┘        └─┘ └┘ └┘  └───┘           └─────────────┘     
par    └─────┘        └─┘ └┘ └┘  └───┘           └──────────────┘     
pid    └───┘└┘        └─┘ └┘   └───┘           └──────────────┘     
st   ─────────────────────────┘└─────────────────┘└───────────────────┘└─
626    rw [(rat.mul_def this one_ne_zero), (mul_comm (q.denom : ℤ) 1), (div_mk_div_cancel_left this)]
id          └─────────┘ └──┘ └─────────┘    └──────┘  └─────┘           └────────────────────┘ └──┘
src    └──┘ └─────────┘    └─────────┘└─┘ └──────┘ └─────┘└─┘ └────┘ └────────────────────┘    └─┘
typ    └──┘ └─────────┘└──┘└─────────┘└─┘ └──────┘ └─────┘└─┘ └────┘ └────────────────────┘└──┘└─┘
doc    └──┘                           └─┘                 └─┘ └────┘                           └─┘
txt    └──┘                           └─┘                 └─┘ └────┘                           └─┘
par    └──┘                           └─┘                 └─┘ └────┘                           └─┘
pid      └┘                           └─┘                 └─┘ └────┘                           └┘
st   ───────────────────────────────────┘└──────────────────────────┘└─────────────────────────────┘
627  end
st   └─┘
628  
629  end rat